src/ZF/OrderArith.thy
changeset 14171 0cab06e3bbd0
parent 14120 3a73850c6c7d
child 16417 9bc16273c2d4
     1.1 --- a/src/ZF/OrderArith.thy	Wed Aug 27 18:22:34 2003 +0200
     1.2 +++ b/src/ZF/OrderArith.thy	Thu Aug 28 01:56:40 2003 +0200
     1.3 @@ -556,7 +556,7 @@
     1.4  text{*As a special case, we have @{term "bij(Pow(A*B), A -> Pow(B))"} *}
     1.5  lemma Pow_Sigma_bij:
     1.6      "(\<lambda>r \<in> Pow(Sigma(A,B)). \<lambda>x \<in> A. r``{x})  
     1.7 -     \<in> bij(Pow(Sigma(A,B)), \<Pi>x \<in> A. Pow(B(x)))"
     1.8 +     \<in> bij(Pow(Sigma(A,B)), \<Pi> x \<in> A. Pow(B(x)))"
     1.9  apply (rule_tac d = "%f. \<Union>x \<in> A. \<Union>y \<in> f`x. {<x,y>}" in lam_bijective)
    1.10  apply (blast intro: lam_type)
    1.11  apply (blast dest: apply_type, simp_all)