let a be Ordinal; :: thesis: for n being Nat holds (n *^ (exp (omega,a))) +^ (exp (omega,a)) = (n *^ (exp (omega,a))) (+) (exp (omega,a))
let n be Nat; :: thesis: (n *^ (exp (omega,a))) +^ (exp (omega,a)) = (n *^ (exp (omega,a))) (+) (exp (omega,a))
A1: exp (omega,a) = 1 *^ (exp (omega,a)) by ORDINAL2:39;
( 0 in 1 & 1 in omega ) by CARD_1:49, TARSKI:def 1;
then omega -exponent (exp (omega,a)) = a by A1, ORDINAL5:58;
hence (n *^ (exp (omega,a))) +^ (exp (omega,a)) = (n *^ (exp (omega,a))) (+) (exp (omega,a)) by Th83; :: thesis: verum