defpred S₁[ Nat] means for a, b being non empty Ordinal st len (CantorNF a) = $1 holds
a +^ b c= a (+) b;
A1: S₁[1]

proof

let a, b be non empty Ordinal; :: thesis: ( len (CantorNF a) = 1 implies a +^ b c= a (+) b )
assume len (CantorNF a) = 1 ; :: thesis: a +^ b c= a (+) b
then A2: CantorNF a = <%((CantorNF a) . 0)%> by AFINSQ_1:34;
0 in dom (CantorNF a) by XBOOLE_1:61, ORDINAL1:11;
then (CantorNF a) . 0 is Cantor-component by ORDINAL5:def 11;
then consider c being Ordinal, m being Nat such that
A3: ( 0 in Segm m & (CantorNF a) . 0 = m *^ (exp (omega,c)) ) by ORDINAL5:def 9;

per cases ( omega -exponent b c= c or c in omega -exponent b ) by ORDINAL1:16;

suppose A4: omega -exponent b c= c ; :: thesis: a +^ b c= a (+) b

a +^ b = (Sum^ (CantorNF a)) +^ b
.= ((CantorNF a) . 0) +^ b by A2, ORDINAL5:53
.= (m *^ (exp (omega,c))) (+) b by A3, A4, Th83
.= (Sum^ (CantorNF a)) (+) b by A2, A3, ORDINAL5:53
.= a (+) b ;
hence a +^ b c= a (+) b ; :: thesis: verum

end;

suppose A5: c in omega -exponent b ; :: thesis: a +^ b c= a (+) b

( 0 in m & m in omega ) by A3, ORDINAL1:def 12;
then omega -exponent ((CantorNF a) . 0) in omega -exponent b by A3, A5, ORDINAL5:58;
then omega -exponent (Sum^ (CantorNF a)) in omega -exponent b by Th44;
then omega *^ a c= b by Th103;
then a +^ b = b by Th30;
hence a +^ b c= a (+) b by Th99; :: thesis: verum

end;

end;

end;

A6: for n being non zero Nat st S₁[n] holds
S₁[n + 1]

proof

let n be non zero Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A7: S₁[n] ; :: thesis: S₁[n + 1]
let a, b be non empty Ordinal; :: thesis: ( len (CantorNF a) = n + 1 implies a +^ b c= a (+) b )
assume A8: len (CantorNF a) = n + 1 ; :: thesis: a +^ b c= a (+) b
consider a0 being Cantor-component Ordinal, A0 being Cantor-normal-form Ordinal-Sequence such that
A9: CantorNF a = <%a0%> ^ A0 by ORDINAL5:67;
A10: n + 1 = (len <%a0%>) + (len A0) by A8, A9, AFINSQ_1:17
.= (len (CantorNF (Sum^ A0))) + 1 by AFINSQ_1:34 ;
then CantorNF (Sum^ A0) <> {} ;
then A11: (Sum^ A0) +^ b c= (Sum^ A0) (+) b by A7, A10;
CantorNF a0 = <%a0%> by Th70;
then len (CantorNF a0) = 1 by AFINSQ_1:34;
then A12: a0 +^ ((Sum^ A0) (+) b) c= a0 (+) ((Sum^ A0) (+) b) by A1;
A13: a = Sum^ (CantorNF a)
.= a0 +^ (Sum^ A0) by A9, ORDINAL5:55
.= (Sum^ <%a0%>) +^ (Sum^ A0) by ORDINAL5:53
.= (Sum^ <%a0%>) (+) (Sum^ A0) by A9, Th84
.= a0 (+) (Sum^ A0) by ORDINAL5:53 ;
a +^ b = (Sum^ (CantorNF a)) +^ b
.= (a0 +^ (Sum^ A0)) +^ b by A9, ORDINAL5:55
.= a0 +^ ((Sum^ A0) +^ b) by ORDINAL3:30 ;
then a +^ b c= a0 +^ ((Sum^ A0) (+) b) by A11, ORDINAL2:33;
then a +^ b c= a0 (+) ((Sum^ A0) (+) b) by A12, XBOOLE_1:1;
hence a +^ b c= a (+) b by A13, Th81; :: thesis: verum

end;

A14: for n being non zero Nat holds S₁[n] from NAT_1:sch 10(A1, A6);
let a, b be Ordinal; :: thesis: a +^ b c= a (+) b

per cases ( a = {} or b = {} or ( a <> {} & b <> {} ) ) ;

suppose a = {} ; :: thesis: a +^ b c= a (+) b

then ( a +^ b = b & a (+) b = b ) by Th82, ORDINAL2:30;
hence a +^ b c= a (+) b ; :: thesis: verum

end;

suppose b = {} ; :: thesis: a +^ b c= a (+) b

then ( a +^ b = a & a (+) b = a ) by Th82, ORDINAL2:27;
hence a +^ b c= a (+) b ; :: thesis: verum

end;

suppose A15: ( a <> {} & b <> {} ) ; :: thesis: a +^ b c= a (+) b

then not len (CantorNF a) is zero ;
hence a +^ b c= a (+) b by A14, A15; :: thesis: verum

end;

end;