theorem Th12: :: CARD_2:13

for A, B being Ordinal holds card (A +^ B) = (card A) +` (card B)