--- a/src/ZF/equalities.ML Thu Feb 26 15:45:33 1998 +0100
+++ b/src/ZF/equalities.ML Fri Feb 27 11:06:28 1998 +0100
@@ -476,6 +476,16 @@
by (Blast_tac 1);
qed "vimage_Int_subset";
+goalw thy [function_def]
+ "!!f. function(f) ==> f-``(A Int B) = (f-``A) Int (f-``B)";
+by (Blast_tac 1);
+qed "function_vimage_Int";
+
+goalw thy [function_def]
+ "!!f. function(f) ==> f-``(A-B) = (f-``A) - (f-``B)";
+by (Blast_tac 1);
+qed "function_vimage_Diff";
+
goal ZF.thy "(r Int A*A)-``B <= (r-``B) Int A";
by (Blast_tac 1);
qed "vimage_Int_square_subset";