# HG changeset patch
# User paulson
# Date 936981424 -7200
# Node ID 5c094aec523d1e2021d0bcd0fcc4d9ae2c90c270
# Parent  599d3414b51d6b760b21bc7e5159bf5454e234e7
new theorem image_image_eq_UN

diff -r 599d3414b51d -r 5c094aec523d src/HOL/Fun.ML
--- 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";