new theorem image_image_eq_UN

--- a/src/HOL/Fun.ML	Fri Sep 10 17:28:51 1999 +0200
+++ b/src/HOL/Fun.ML	Fri Sep 10 18:37:04 1999 +0200
@@ -67,6 +67,10 @@
 by (Blast_tac 1);
 qed "image_compose";
 
+Goal "f``g``A = (UN x:A. {f (g x)})";
+by (Blast_tac 1);
+qed "image_image_eq_UN";
+
 Goalw [o_def] "UNION A (g o f) = UNION (f``A) g";
 by (Blast_tac 1);
 qed "UN_o";