defpred S₁[ Nat] means for A, B being finite Ordinal-Sequence st len A = $1 & A ^ B is Cantor-normal-form holds
(Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B);
A1: S₁[ 0 ]

proof

let A, B be finite Ordinal-Sequence; :: thesis: ( len A = 0 & A ^ B is Cantor-normal-form implies (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B) )
assume ( len A = 0 & A ^ B is Cantor-normal-form ) ; :: thesis: (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)
then A is empty ;
then A2: Sum^ A = 0 by ORDINAL5:52;
hence (Sum^ A) (+) (Sum^ B) = Sum^ B by Th82
.= (Sum^ A) +^ (Sum^ B) by A2, ORDINAL2:30 ;
:: thesis: verum

end;

A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A4: S₁[n] ; :: thesis: S₁[n + 1]
let A, B be finite Ordinal-Sequence; :: thesis: ( len A = n + 1 & A ^ B is Cantor-normal-form implies (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B) )
assume A5: ( len A = n + 1 & A ^ B is Cantor-normal-form ) ; :: thesis: (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)
then A6: ( A <> {} & A is Cantor-normal-form ) by ORDINAL5:66;
then consider a0 being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A7: A = <%a0%> ^ A0 by ORDINAL5:67;
A8: <%a0%> ^ (A0 ^ B) is Cantor-normal-form by A5, A7, AFINSQ_1:27;
then A9: A0 ^ B is Cantor-normal-form by ORDINAL5:66;
n + 1 = (len <%a0%>) + (len A0) by A5, A7, AFINSQ_1:17
.= 1 + (len A0) by AFINSQ_1:34 ;
then A10: (Sum^ A0) (+) (Sum^ B) = (Sum^ A0) +^ (Sum^ B) by A4, A9;
consider b being Ordinal, m being Nat such that
A11: ( 0 in Segm m & a0 = m *^ (exp (omega,b)) ) by ORDINAL5:def 9;
reconsider m = m as non zero Nat by A11;
( 0 in m & m in omega ) by A11, ORDINAL1:def 12;
then A12: omega -exponent a0 = b by A11, ORDINAL5:58;
A13: omega -exponent (Sum^ A0) c= b

proof

per cases ( 0 in Sum^ A0 or not 0 in Sum^ A0 ) ;

suppose A14: 0 in Sum^ A0 ; :: thesis: omega -exponent (Sum^ A0) c= b

Sum^ A0 in exp (omega,(omega -exponent a0)) by A6, A7, Th43;
hence omega -exponent (Sum^ A0) c= b by A12, A14, Th23, ORDINAL1:def 2; :: thesis: verum

end;

suppose not 0 in Sum^ A0 ; :: thesis: omega -exponent (Sum^ A0) c= b

then omega -exponent (Sum^ A0) = 0 by ORDINAL5:def 10;
hence omega -exponent (Sum^ A0) c= b ; :: thesis: verum

end;

end;

end;

A15: omega -exponent ((Sum^ A0) (+) (Sum^ B)) c= b

proof

A16: (Sum^ A0) (+) (Sum^ B) = Sum^ (A0 ^ B) by A10, Th24;

per cases ( 0 in Sum^ (A0 ^ B) or not 0 in Sum^ (A0 ^ B) ) ;

suppose A17: 0 in Sum^ (A0 ^ B) ; :: thesis: omega -exponent ((Sum^ A0) (+) (Sum^ B)) c= b

Sum^ (A0 ^ B) in exp (omega,(omega -exponent a0)) by A8, Th43;
hence omega -exponent ((Sum^ A0) (+) (Sum^ B)) c= b by A12, A16, A17, Th23, ORDINAL1:def 2; :: thesis: verum

end;

suppose not 0 in Sum^ (A0 ^ B) ; :: thesis: omega -exponent ((Sum^ A0) (+) (Sum^ B)) c= b

then omega -exponent (Sum^ (A0 ^ B)) = 0 by ORDINAL5:def 10;
hence omega -exponent ((Sum^ A0) (+) (Sum^ B)) c= b by A16; :: thesis: verum

end;

end;

end;

thus (Sum^ A) (+) (Sum^ B) = (a0 +^ (Sum^ A0)) (+) (Sum^ B) by A7, ORDINAL5:55
.= (a0 (+) (Sum^ A0)) (+) (Sum^ B) by A11, A13, Th83
.= a0 (+) ((Sum^ A0) (+) (Sum^ B)) by Th81
.= a0 +^ ((Sum^ A0) (+) (Sum^ B)) by A11, A15, Th83
.= (a0 +^ (Sum^ A0)) +^ (Sum^ B) by A10, ORDINAL3:30
.= (Sum^ A) +^ (Sum^ B) by A7, ORDINAL5:55 ; :: thesis: verum

end;

A18: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let A, B be finite Ordinal-Sequence; :: thesis: ( A ^ B is Cantor-normal-form implies (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B) )
assume A19: A ^ B is Cantor-normal-form ; :: thesis: (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B)
len A is Nat ;
hence (Sum^ A) (+) (Sum^ B) = (Sum^ A) +^ (Sum^ B) by A18, A19; :: thesis: verum