theorem Th71: :: CARD_2:72

for A being Ordinal ex n being Nat st A *^ (succ 1) = A +^ n