defpred S₁[ Nat] means for A being Cantor-normal-form Ordinal-Sequence st len A = $1 holds
omega -exponent (Sum^ A) = omega -exponent (A . 0);
A1: S₁[ 0 ]

proof

let A be Cantor-normal-form Ordinal-Sequence; :: thesis: ( len A = 0 implies omega -exponent (Sum^ A) = omega -exponent (A . 0) )
assume len A = 0 ; :: thesis: omega -exponent (Sum^ A) = omega -exponent (A . 0)
then A = {} ;
hence omega -exponent (Sum^ A) = omega -exponent (A . 0) by ORDINAL5:52; :: 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 be Cantor-normal-form Ordinal-Sequence; :: thesis: ( len A = n + 1 implies omega -exponent (Sum^ A) = omega -exponent (A . 0) )
assume A5: len A = n + 1 ; :: thesis: omega -exponent (Sum^ A) = omega -exponent (A . 0)
then A <> {} ;
then consider c being Cantor-component Ordinal, B being Cantor-normal-form Ordinal-Sequence such that
A6: A = <%c%> ^ B by ORDINAL5:67;

per cases ( B = {} or B <> {} ) ;

suppose A7: B = {} ; :: thesis: omega -exponent (Sum^ A) = omega -exponent (A . 0)

Sum^ A = c +^ (Sum^ B) by A6, ORDINAL5:55
.= A . 0 by A6, A7, ORDINAL5:52, ORDINAL2:27 ;
hence omega -exponent (Sum^ A) = omega -exponent (A . 0) ; :: thesis: verum

end;

suppose A8: B <> {} ; :: thesis: omega -exponent (Sum^ A) = omega -exponent (A . 0)

then {} c< dom B by XBOOLE_1:2, XBOOLE_0:def 8;
then A9: 0 in dom B by ORDINAL1:11;
n + 1 = (len <%c%>) + (len B) by A5, A6, AFINSQ_1:17
.= (len B) + 1 by AFINSQ_1:34 ;
then A10: omega -exponent (Sum^ B) = omega -exponent (B . 0) by A4;
A . ((len <%c%>) + 0) = B . 0 by A6, A9, AFINSQ_1:def 3;
then A11: A . 1 = B . 0 by AFINSQ_1:34;
(len <%c%>) + 0 in dom A by A6, A9, AFINSQ_1:23;
then A12: 1 in dom A by AFINSQ_1:34;
0 in 1 by CARD_1:49, TARSKI:def 1;
then A13: omega -exponent (Sum^ B) in omega -exponent (A . 0) by A10, A11, A12, ORDINAL5:def 11;
A14: omega -exponent (A . 0) c= omega -exponent (Sum^ A) by Th22, ORDINAL5:56;
consider d being Ordinal, m being Nat such that
A15: ( 0 in Segm m & c = m *^ (exp (omega,d)) ) by ORDINAL5:def 9;
( 0 in m & m in omega ) by A15, ORDINAL1:def 12;
then omega -exponent c = d by A15, ORDINAL5:58;
then A16: omega -exponent (A . 0) = d by A6, AFINSQ_1:35;
assume omega -exponent (Sum^ A) <> omega -exponent (A . 0) ; :: thesis: contradiction
then omega -exponent (A . 0) in omega -exponent (Sum^ A) by A14, XBOOLE_0:def 8, ORDINAL1:11;
then A17: exp (omega,d) in exp (omega,(omega -exponent (Sum^ A))) by A16, ORDINAL4:24;
then A18: c in exp (omega,(omega -exponent (Sum^ A))) by A15, Th42;
set e = omega -exponent (Sum^ B);
A19: 0 in Sum^ B

proof

assume not 0 in Sum^ B ; :: thesis: contradiction
then Sum^ B c= 0 by ORDINAL1:16;
hence contradiction by A8; :: thesis: verum

end;

A20: Sum^ B in exp (omega,(succ (omega -exponent (Sum^ B))))

proof

assume not Sum^ B in exp (omega,(succ (omega -exponent (Sum^ B)))) ; :: thesis: contradiction
then exp (omega,(succ (omega -exponent (Sum^ B)))) c= Sum^ B by ORDINAL1:16;
then succ (omega -exponent (Sum^ B)) c= omega -exponent (Sum^ B) by A19, ORDINAL5:def 10;
hence contradiction by ORDINAL1:5, ORDINAL1:6; :: thesis: verum

end;

exp (omega,(succ (omega -exponent (Sum^ B)))) c= exp (omega,d) by A13, A16, ORDINAL1:21, ORDINAL4:27;
then Sum^ B in exp (omega,(omega -exponent (Sum^ A))) by A17, A20, ORDINAL1:10;
then c +^ (Sum^ B) in exp (omega,(omega -exponent (Sum^ A))) by A18, Th40;
then A22: Sum^ A in exp (omega,(omega -exponent (Sum^ A))) by A6, ORDINAL5:55;
Sum^ B c= c +^ (Sum^ B) by ORDINAL3:24;
then Sum^ B c= Sum^ A by A6, ORDINAL5:55;
then exp (omega,(omega -exponent (Sum^ A))) c= Sum^ A by A19, ORDINAL5:def 10;
then Sum^ A in Sum^ A by A22;
hence contradiction ; :: thesis: verum

end;

end;

end;

A23: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A3);
let A be Cantor-normal-form Ordinal-Sequence; :: thesis: omega -exponent (Sum^ A) = omega -exponent (A . 0)
len A is Nat ;
hence omega -exponent (Sum^ A) = omega -exponent (A . 0) by A23; :: thesis: verum