let A, B be Ordinal; :: thesis: card (A +^ B) = (card A) +` (card B)
A1: A +^ B,H<sub>3</sub>(A,B) are_equipotent by Lm1;
( A, card A are_equipotent & B, card B are_equipotent ) by CARD_1:def 2;
then A2: H<sub>3</sub>(A,B),H<sub>3</sub>( card A, card B) are_equipotent by Th11;
H<sub>3</sub>( card A, card B),(card A) +^ (card B) are_equipotent by Lm1;
then H<sub>3</sub>(A,B),(card A) +^ (card B) are_equipotent by A2, WELLORD2:15;
then A +^ B,(card A) +^ (card B) are_equipotent by A1, WELLORD2:15;
hence card (A +^ B) = (card A) +` (card B) by CARD_1:5; :: thesis: verum