theorem Th36: :: CARD_2:37

for m, n being Nat holds n * m = n *^ m