--- a/src/ZF/OrderArith.thy Wed Aug 27 18:22:34 2003 +0200
+++ b/src/ZF/OrderArith.thy Thu Aug 28 01:56:40 2003 +0200
@@ -556,7 +556,7 @@
text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
lemma Pow_Sigma_bij:
"(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})
- \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
+ \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
apply (blast intro: lam_type)
apply (blast dest: apply_type, simp_all)