let A, B be Ordinal; :: thesis: card (A +^ B) = (card A) +` (card B)
A1: ( (card A) +^ (card B),H<sub>3</sub>( card A, card B) are_equipotent & A +^ B,H<sub>3</sub>(A,B) are_equipotent ) by Lm1;
( A, card A are_equipotent & B, card B are_equipotent & card A = card A & card B = card B & 0 <> 1 ) by CARD_1:def 5;
then ( H<sub>3</sub>( card A, card B),(card A) +^ (card B) are_equipotent & H<sub>3</sub>(A,B),H<sub>3</sub>( card A, card B) are_equipotent ) by Lm1, Th23;
then H<sub>3</sub>(A,B),(card A) +^ (card B) are_equipotent by WELLORD2:22;
then ( (card A) +` (card B) = card ((card A) +^ (card B)) & A +^ B,(card A) +^ (card B) are_equipotent ) by A1, WELLORD2:22;
hence card (A +^ B) = (card A) +` (card B) by CARD_1:21; :: thesis: verum