new theorem image_Union_eq

--- a/src/HOL/equalities.ML	Sat Feb 13 22:08:54 1999 +0100
+++ b/src/HOL/equalities.ML	Tue Feb 16 10:50:35 1999 +0100
@@ -502,6 +502,10 @@
 by (Blast_tac 1);
 qed "Union_image_eq";
 
+Goal "f `` Union S = (UN x:S. f `` x)";
+by (Blast_tac 1);
+qed "image_Union_eq";
+
 Goal "Inter(B``A) = (INT x:A. B(x))";
 by (Blast_tac 1);
 qed "Inter_image_eq";