theorem Th35: :: CARD_2:36

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