theorem Th13: :: CARD_2:14

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