hence Uls: "\<Union>A \<prec> c" using jls

     have  "c \<lesssim> \<Union>A" using c

       by (blast intro: eqpoll_sym eqpoll_imp_lepoll lesspoll_trans1)

     moreover have  "c \<lesssim> \<Union>A" using c

     ultimately have "c \<prec> c"

     also have "... \<approx> j"  by (rule eqpoll_sym [OF eqp])

       by (blast intro: lesspoll_trans1) 

     also have "... \<prec> c"  by (rule jls)

     finally have "c \<prec> c" .

 (*Unconditional version requires AC*)

 text{*Unconditional version requires AC*}

     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]

   assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"

      ==> (i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"

   shows "(i \<oplus> j) \<oplus> k = i \<oplus> (j \<oplus> k)"

 apply (unfold cadd_def)

 proof (unfold cadd_def, rule cardinal_cong)

 apply (rule cardinal_cong)

   have "|i + j| + k \<approx> (i + j) + k"

 apply (rule eqpoll_trans)

     by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 

  apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])

   also have "...  \<approx> i + (j + k)"

  apply (blast intro: well_ord_radd )

     by (rule sum_assoc_eqpoll) 

 apply (rule sum_assoc_eqpoll [THEN eqpoll_trans])

   also have "...  \<approx> i + |j + k|"

 apply (rule eqpoll_sym)

     by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd j k eqpoll_sym) 

 apply (rule sum_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])

   finally show "|i + j| + k \<approx> i + |j + k|" .

 apply (blast intro: well_ord_radd )

 qed

 done

 (*Unconditional version requires AC*)

 text{*Unconditional version requires AC*}

     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]

   assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"

      ==> (i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"

   shows "(i \<otimes> j) \<otimes> k = i \<otimes> (j \<otimes> k)"

 apply (unfold cmult_def)

 proof (unfold cmult_def, rule cardinal_cong)

 apply (rule cardinal_cong)

   have "|i * j| * k \<approx> (i * j) * k"

 apply (rule eqpoll_trans)

     by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult i j) 

  apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])

   also have "...  \<approx> i * (j * k)"

  apply (blast intro: well_ord_rmult)

     by (rule prod_assoc_eqpoll) 

 apply (rule prod_assoc_eqpoll [THEN eqpoll_trans])

   also have "...  \<approx> i * |j * k|"

 apply (rule eqpoll_sym)

     by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_rmult j k eqpoll_sym) 

 apply (rule prod_eqpoll_cong [OF eqpoll_refl well_ord_cardinal_eqpoll])

   finally show "|i * j| * k \<approx> i * |j * k|" .

 apply (blast intro: well_ord_rmult)

 qed

 done

     "[| well_ord(i,ri); well_ord(j,rj); well_ord(k,rk) |]

   assumes i: "well_ord(i,ri)" and j: "well_ord(j,rj)" and k: "well_ord(k,rk)"

      ==> (i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"

   shows "(i \<oplus> j) \<otimes> k = (i \<otimes> k) \<oplus> (j \<otimes> k)"

 apply (unfold cadd_def cmult_def)

 proof (unfold cadd_def cmult_def, rule cardinal_cong)

 apply (rule cardinal_cong)

   have "|i + j| * k \<approx> (i + j) * k"

 apply (rule eqpoll_trans)

     by (blast intro: prod_eqpoll_cong well_ord_cardinal_eqpoll eqpoll_refl well_ord_radd i j) 

  apply (rule prod_eqpoll_cong [OF well_ord_cardinal_eqpoll eqpoll_refl])

   also have "...  \<approx> i * k + j * k"

 apply (blast intro: well_ord_radd)

     by (rule sum_prod_distrib_eqpoll) 

 apply (rule sum_prod_distrib_eqpoll [THEN eqpoll_trans])

   also have "...  \<approx> |i * k| + |j * k|"

 apply (rule eqpoll_sym)

     by (blast intro: sum_eqpoll_cong well_ord_cardinal_eqpoll well_ord_rmult i j k eqpoll_sym) 

 apply (rule sum_eqpoll_cong [OF well_ord_cardinal_eqpoll

   finally show "|i + j| * k \<approx> |i * k| + |j * k|" .

                                 well_ord_cardinal_eqpoll])

 qed

 apply (blast intro: well_ord_rmult)+

 done

 lemma sum_lepoll_prod: "2 \<lesssim> C ==> B+B \<lesssim> C*B"

 lemma sum_lepoll_prod: 

 apply (rule lepoll_trans)

   assumes C: "2 \<lesssim> C" shows "B+B \<lesssim> C*B"

 apply (rule sum_eq_2_times [THEN equalityD1, THEN subset_imp_lepoll])

 proof -

 apply (erule prod_lepoll_mono)

   have "B+B \<lesssim> 2*B"

 apply (rule lepoll_refl)

     by (simp add: sum_eq_2_times) 

 done

   also have "... \<lesssim> C*B"

     by (blast intro: prod_lepoll_mono lepoll_refl C) 

   finally show "B+B \<lesssim> C*B" .

 qed

 lemma csquare_lam_inj:

 lemma well_ord_csquare: 

      "Ord(K) ==> (lam <x,y>:K*K. <x \<union> y, x, y>) \<in> inj(K*K, K*K*K)"

   assumes K: "Ord(K)" shows "well_ord(K*K, csquare_rel(K))"

 apply (unfold inj_def)

 proof (unfold csquare_rel_def, rule well_ord_rvimage)

 apply (force intro: lam_type Un_least_lt [THEN ltD] ltI)

   show "(\<lambda>\<langle>x,y\<rangle>\<in>K \<times> K. \<langle>x \<union> y, x, y\<rangle>) \<in> inj(K \<times> K, K \<times> K \<times> K)" using K

 done

     by (force simp add: inj_def intro: lam_type Un_least_lt [THEN ltD] ltI)

 next

 lemma well_ord_csquare: "Ord(K) ==> well_ord(K*K, csquare_rel(K))"

   show "well_ord(K \<times> K \<times> K, rmult(K, Memrel(K), K \<times> K, rmult(K, Memrel(K), K, Memrel(K))))"

 apply (unfold csquare_rel_def)

     using K by (blast intro: well_ord_rmult well_ord_Memrel)

 apply (rule csquare_lam_inj [THEN well_ord_rvimage], assumption)

 qed

 apply (blast intro: well_ord_rmult well_ord_Memrel)

 done

 apply (safe del: SigmaI succCI)

 apply (safe del: SigmaI dest!: csquareD)

 apply (erule csquareD [THEN conjE])

 (*Kunen: "each <x,y>: K*K has no more than z*z predecessors..." (page 29) *)

 text{*Kunen: "each @{term"\<langle>x,y\<rangle> \<in> K \<times> K"} has no more than @{term"z \<times> z"} predecessors..." (page 29) *}

   "[| Limit(K);  x<K;  y<K;  z=succ(x \<union> y) |]

   assumes K: "Limit(K)" and x: "x<K" and y: " y<K" and z: "z=succ(x \<union> y)"

    ==> | ordermap(K*K, csquare_rel(K)) ` <x,y> | \<le> |succ(z)| \<otimes> |succ(z)|"

   shows "|ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle>| \<le> |succ(z)| \<otimes> |succ(z)|"

 apply (unfold cmult_def)

 proof (unfold cmult_def, rule well_ord_lepoll_imp_Card_le)

 apply (rule well_ord_rmult [THEN well_ord_lepoll_imp_Card_le])

   show "well_ord(|succ(z)| \<times> |succ(z)|, 

 apply (rule Ord_cardinal [THEN well_ord_Memrel])+

                  rmult(|succ(z)|, Memrel(|succ(z)|), |succ(z)|, Memrel(|succ(z)|)))"

 apply (subgoal_tac "z<K")

     by (blast intro: Ord_cardinal well_ord_Memrel well_ord_rmult) 

  prefer 2 apply (blast intro!: Un_least_lt Limit_has_succ)

 next

 apply (rule ordermap_z_lt [THEN leI, THEN le_imp_lepoll, THEN lepoll_trans],

   have zK: "z<K" using x y z K 

        assumption+)

     by (blast intro: Un_least_lt Limit_has_succ)

 apply (rule ordermap_eqpoll_pred [THEN eqpoll_imp_lepoll, THEN lepoll_trans])

   hence oz: "Ord(z)" by (elim ltE) 

 apply (erule Limit_is_Ord [THEN well_ord_csquare])

   have "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> ordermap(K \<times> K, csquare_rel(K)) ` \<langle>z,z\<rangle>"

 apply (blast intro: ltD)

     by (blast intro: ordermap_z_lt leI le_imp_lepoll K x y z) 

 apply (rule pred_csquare_subset [THEN subset_imp_lepoll, THEN lepoll_trans],

   also have "... \<approx>  Order.pred(K \<times> K, \<langle>z,z\<rangle>, csquare_rel(K))"

             assumption)

     proof (rule ordermap_eqpoll_pred)

 apply (elim ltE)

       show "well_ord(K \<times> K, csquare_rel(K))" using K 

 apply (rule prod_eqpoll_cong [THEN eqpoll_sym, THEN eqpoll_imp_lepoll])

         by (rule Limit_is_Ord [THEN well_ord_csquare])

 apply (erule Ord_succ [THEN Ord_cardinal_eqpoll])+

     next

 done

       show "\<langle>z, z\<rangle> \<in> K \<times> K" using zK

         by (blast intro: ltD)

 (*Kunen: "... so the order type is @{text"\<le>"} K" *)

     qed

   also have "...  \<lesssim> succ(z) \<times> succ(z)" using zK

     by (rule pred_csquare_subset [THEN subset_imp_lepoll])

   also have "... \<approx> |succ(z)| \<times> |succ(z)|" using oz

     by (blast intro: prod_eqpoll_cong Ord_succ Ord_cardinal_eqpoll eqpoll_sym) 

   finally show "ordermap(K \<times> K, csquare_rel(K)) ` \<langle>x,y\<rangle> \<lesssim> |succ(z)| \<times> |succ(z)|" .

 qed

 text{*Kunen: "... so the order type is @{text"\<le>"} K" *}