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