let a be Ordinal; for n, m being Nat holds (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))
let n, m be Nat; (n *^ (exp (omega,a))) (+) (m *^ (exp (omega,a))) = (n + m) *^ (exp (omega,a))
per cases
( n = 0 or n <> 0 )
;
suppose A2:
n <> 0
;
(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
;
verum end; end;