let a be Ordinal; :: thesis: for n, m being Nat holds (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))
let n, m be Nat; :: thesis: (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))

per cases ( n = 0 or n <> 0 ) ;

suppose A1: n = 0 ; :: thesis: (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))

hence (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = 0 (+) (m *^ (exp (omega,a))) by ORDINAL2:35
.= (n + m) *^ (exp (omega,a)) by A1, Th82 ;
:: thesis: verum

end;

suppose A2: n <> 0 ; :: thesis: (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))

then A3: ( 0 in n & n in omega ) by XBOOLE_1:61, ORDINAL1:11, ORDINAL1:def 12;
omega -exponent (last (CantorNF (n *^ (exp (omega,a))))) = omega -exponent (last ({} ^ <%(n *^ (exp (omega,a)))%>)) by A2, Th69
.= omega -exponent (n *^ (exp (omega,a))) by AFINSQ_1:92
.= a by A3, ORDINAL5:58 ;
hence (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n *^ (exp (omega,a))) +^ (m *^ (exp (omega,a))) by Th86
.= (n +^ m) *^ (exp (omega,a)) by ORDINAL3:46
.= (n + m) *^ (exp (omega,a)) by CARD_2:36 ;
:: thesis: verum

end;

end;