new thm vimage_image_eq

--- a/src/HOL/Fun.ML	Sat Oct 16 18:56:09 1999 +0200
+++ b/src/HOL/Fun.ML	Mon Oct 18 15:16:10 1999 +0200
@@ -253,6 +253,10 @@
 qed "vimage_id";
 Addsimps [vimage_ident, vimage_id];
 
+Goal "f -`` (f `` A) = {y. EX x:A. f x = f y}";
+by (blast_tac (claset() addIs [sym]) 1);
+qed "vimage_image_eq";
+
 Goal "f``(A Int B) <= f``A Int f``B";
 by (Blast_tac 1);
 qed "image_Int_subset";