for a, b being Ordinal
for n being Nat st omega -exponent a c= b holds
(n *^ (exp (omega,b))) (+) a = (n *^ (exp (omega,b))) +^ a