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

proof

let A, B be Cantor-normal-form Ordinal-Sequence; :: thesis: ( (dom A) \/ (dom B) = 0 & Sum^ A = Sum^ B implies A = B )
assume ( (dom A) \/ (dom B) = 0 & Sum^ A = Sum^ B ) ; :: thesis: A = B
then ( A is empty & B is empty ) ;
hence A = B ; :: thesis: verum

end;

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

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
let A, B be Cantor-normal-form Ordinal-Sequence; :: thesis: ( (dom A) \/ (dom B) = n + 1 & Sum^ A = Sum^ B implies A = B )
assume A4: ( (dom A) \/ (dom B) = n + 1 & Sum^ A = Sum^ B ) ; :: thesis: A = B
dom A <> {}

proof

assume A5: dom A = {} ; :: thesis: contradiction
then A is empty ;
then B = {} by A4, ORDINAL5:52;
hence contradiction by A4, A5; :: thesis: verum

end;

then A6: A <> {} ;
dom B <> {}

proof

assume dom B = {} ; :: thesis: contradiction
then B is empty ;
hence contradiction by A4, A6, ORDINAL5:52; :: thesis: verum

end;

then B <> {} ;
then consider b being Cantor-component Ordinal, B0 being Cantor-normal-form Ordinal-Sequence such that
A7: B = <%b%> ^ B0 by ORDINAL5:67;
consider a being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A8: A = <%a%> ^ A0 by A6, ORDINAL5:67;
A9: a +^ (Sum^ A0) = Sum^ B by A4, A8, ORDINAL5:55
.= b +^ (Sum^ B0) by A7, ORDINAL5:55 ;
A10: a = b

proof

A11: ( A . 0 = a & B . 0 = b ) by A7, A8, AFINSQ_1:35;
then A12: omega -exponent a = omega -exponent (Sum^ B) by A4, Th44
.= omega -exponent b by A11, Th44 ;
consider d1 being Ordinal, n1 being Nat such that
A13: ( 0 in Segm n1 & a = n1 *^ (exp (omega,d1)) ) by ORDINAL5:def 9;
consider d2 being Ordinal, n2 being Nat such that
A14: ( 0 in Segm n2 & b = n2 *^ (exp (omega,d2)) ) by ORDINAL5:def 9;
( 0 in n1 & n1 in omega ) by A13, ORDINAL1:def 12;
then A15: omega -exponent a = d1 by A13, ORDINAL5:58;
( 0 in n2 & n2 in omega ) by A14, ORDINAL1:def 12;
then A16: omega -exponent b = d2 by A14, ORDINAL5:58;
then A17: d1 = d2 by A12, A15;
assume a <> b ; :: thesis: contradiction

per cases then ( a in b or b in a ) by ORDINAL1:14;

suppose A18: a in b ; :: thesis: contradiction

then a +^ (Sum^ A0) = (a +^ (b -^ a)) +^ (Sum^ B0) by A9, ORDINAL3:51
.= a +^ ((b -^ a) +^ (Sum^ B0)) by ORDINAL3:30 ;
then A19: Sum^ A0 = (b -^ a) +^ (Sum^ B0) by ORDINAL3:21;
A20: n1 in n2 by A13, A14, A17, A18, ORDINAL3:34;
A21: b -^ a = (n2 -^ n1) *^ (exp (omega,d1)) by A13, A14, A17, ORDINAL3:63;
( 0 in n2 -^ n1 & n2 -^ n1 in omega ) by A20, ORDINAL3:55, ORDINAL1:def 12;
then A22: omega -exponent (b -^ a) = d1 by A21, ORDINAL5:58;
A23: b -^ a c= (b -^ a) +^ (Sum^ B0) by ORDINAL3:24;
then A24: d1 c= omega -exponent (Sum^ A0) by A19, A22, Th22;
0 in b -^ a by A18, ORDINAL3:55;
then A25: 0 in Sum^ A0 by A19, A23;
Sum^ A0 in exp (omega,(omega -exponent a)) by A8, Th43;
hence contradiction by A15, A24, A25, Th23, ORDINAL1:5; :: thesis: verum

end;

suppose A26: b in a ; :: thesis: contradiction

then b +^ (Sum^ B0) = (b +^ (a -^ b)) +^ (Sum^ A0) by A9, ORDINAL3:51
.= b +^ ((a -^ b) +^ (Sum^ A0)) by ORDINAL3:30 ;
then A27: Sum^ B0 = (a -^ b) +^ (Sum^ A0) by ORDINAL3:21;
A28: n2 in n1 by A13, A14, A17, A26, ORDINAL3:34;
A29: a -^ b = (n1 -^ n2) *^ (exp (omega,d1)) by A13, A14, A17, ORDINAL3:63;
( 0 in n1 -^ n2 & n1 -^ n2 in omega ) by A28, ORDINAL3:55, ORDINAL1:def 12;
then A30: omega -exponent (a -^ b) = d1 by A29, ORDINAL5:58;
A31: a -^ b c= (a -^ b) +^ (Sum^ A0) by ORDINAL3:24;
then A32: d1 c= omega -exponent (Sum^ B0) by A27, A30, Th22;
0 in a -^ b by A26, ORDINAL3:55;
then A33: 0 in Sum^ B0 by A27, A31;
Sum^ B0 in exp (omega,(omega -exponent b)) by A7, Th43;
hence contradiction by A16, A17, A32, A33, Th23, ORDINAL1:5; :: thesis: verum

end;

end;

end;

then A34: Sum^ A0 = Sum^ B0 by A9, ORDINAL3:21;
(dom A0) \/ (dom B0) = ((max ((len A0),(len B0))) + 1) - 1
.= (max (((len A0) + 1),((len B0) + 1))) - 1 by FUZZY_2:42
.= (max (((len A0) + (len <%a%>)),((len B0) + 1))) - 1 by AFINSQ_1:34
.= (max (((len A0) + (len <%a%>)),((len B0) + (len <%b%>)))) - 1 by AFINSQ_1:34
.= (max ((len A),((len B0) + (len <%b%>)))) - 1 by A8, AFINSQ_1:17
.= (max ((len A),(len B))) - 1 by A7, AFINSQ_1:17
.= n by A4 ;
hence A = B by A3, A7, A8, A10, A34; :: thesis: verum

end;

A35: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let A, B be Cantor-normal-form Ordinal-Sequence; :: thesis: ( Sum^ A = Sum^ B implies A = B )
assume A36: Sum^ A = Sum^ B ; :: thesis: A = B
(dom A) \/ (dom B) is natural ;
hence A = B by A35, A36; :: thesis: verum