defpred S1[ Nat] means for a, b being non empty Ordinal st len (CantorNF a) = $1 holds
a +^ b c= a (+) b;
A1: S1[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;
end;
end;
A6: for n being non zero Nat st S1[n] holds
S1[n + 1]
proof
let n be non zero Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; :: thesis: S1[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 S1[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;