diff -r 8f4680be79cc -r 85d3c0981a16 src/ZF/func.thy
--- a/src/ZF/func.thy	Wed May 22 18:55:47 2002 +0200
+++ b/src/ZF/func.thy	Wed May 22 19:34:01 2002 +0200
@@ -233,9 +233,13 @@
 lemma image_lam: "C <= A ==> (lam x:A. b(x)) `` C = {b(x). x:C}"
 by (unfold lam_def, blast)
 
+lemma image_function:
+     "[| function(f);  C <= domain(f) |] ==> f``C = {f`x. x:C}";
+by (blast dest: function_apply_equality intro: function_apply_Pair) 
+
 lemma image_fun: "[| f : Pi(A,B);  C <= A |] ==> f``C = {f`x. x:C}"
-apply (erule eta [THEN subst])
-apply (simp add: image_lam subset_iff)
+apply (simp add: Pi_iff) 
+apply (blast intro: image_function) 
 done
 
 lemma Pi_image_cons:
@@ -323,6 +327,10 @@
 apply (blast intro!: rel_Union function_Union)
 done
 
+lemma gen_relation_Union [rule_format]:
+     "\<forall>f\<in>F. relation(f) \<Longrightarrow> relation(Union(F))"
+by (simp add: relation_def) 
+
 
 (** The Union of 2 disjoint functions is a function **)