let a, b, c be Ordinal; :: thesis: ( b in c implies a (+) b in a (+) c )
assume A1: b in c ; :: thesis: a (+) b in a (+) c

per cases ( a = 0 or a <> 0 ) ;

suppose a = 0 ; :: thesis: a (+) b in a (+) c

then ( a (+) b = b & a (+) c = c ) by Th82;
hence a (+) b in a (+) c by A1; :: thesis: verum

end;

suppose A2: a <> 0 ; :: thesis: a (+) b in a (+) c

defpred S₁[ Nat] means (CantorNF b) . $1 <> (CantorNF c) . $1;
A3: ex i being Nat st S₁[i]

proof

assume A4: for i being Nat holds not S₁[i] ; :: thesis: contradiction
A5: dom (CantorNF b) = dom (CantorNF c)

proof

assume dom (CantorNF b) <> dom (CantorNF c) ; :: thesis: contradiction

per cases then ( not dom (CantorNF b) c= dom (CantorNF c) or not dom (CantorNF c) c= dom (CantorNF b) ) by XBOOLE_0:def 10;

suppose not dom (CantorNF b) c= dom (CantorNF c) ; :: thesis: contradiction

then A6: (CantorNF b) . (dom (CantorNF c)) <> {} by ORDINAL1:16, FUNCT_1:def 9;
not dom (CantorNF c) in dom (CantorNF c) ;
then (CantorNF c) . (dom (CantorNF c)) = {} by FUNCT_1:def 2;
hence contradiction by A4, A6; :: thesis: verum

end;

suppose not dom (CantorNF c) c= dom (CantorNF b) ; :: thesis: contradiction

then A7: (CantorNF c) . (dom (CantorNF b)) <> {} by ORDINAL1:16, FUNCT_1:def 9;
not dom (CantorNF b) in dom (CantorNF b) ;
then (CantorNF b) . (dom (CantorNF b)) = {} by FUNCT_1:def 2;
hence contradiction by A4, A7; :: thesis: verum

end;

end;

end;

for x being object st x in dom (CantorNF b) holds
(CantorNF b) . x = (CantorNF c) . x by A4;
then Sum^ (CantorNF b) = Sum^ (CantorNF c) by A5, FUNCT_1:2;
hence contradiction by A1; :: thesis: verum

end;

consider i being Nat such that
A8: ( S₁[i] & ( for j being Nat st S₁[j] holds
i <= j ) ) from NAT_1:sch 5(A3);
set A1 = (CantorNF b) | i;
set A2 = (CantorNF c) | i;
set B1 = (CantorNF b) /^ i;
set B2 = (CantorNF c) /^ i;
A9: ( i c= dom (CantorNF b) & i c= dom (CantorNF c) )

proof

assume ( not i c= dom (CantorNF b) or not i c= dom (CantorNF c) ) ; :: thesis: contradiction

per cases then ( not i c= dom (CantorNF b) or not i c= dom (CantorNF c) ) ;

suppose A10: not i c= dom (CantorNF b) ; :: thesis: contradiction

then consider x being object such that
A11: ( x in i & not x in dom (CantorNF b) ) by TARSKI:def 3;
i in omega by ORDINAL1:def 12;
then x in omega by A11, ORDINAL1:10;
then reconsider x = x as Nat ;
A12: (CantorNF b) . x = {} by A11, FUNCT_1:def 2;
x in Segm i by A11;
then (CantorNF b) . x = (CantorNF c) . x by A8, NAT_1:44;
then dom (CantorNF c) c= x by A12, FUNCT_1:def 9, ORDINAL1:16;
then dom (CantorNF c) in i by A11, ORDINAL1:12;
then A13: (CantorNF c) . i = {} by FUNCT_1:def 2;
dom (CantorNF b) in i by A10, ORDINAL1:16;
hence contradiction by A8, A13, FUNCT_1:def 2; :: thesis: verum

end;

suppose A14: not i c= dom (CantorNF c) ; :: thesis: contradiction

then consider x being object such that
A15: ( x in i & not x in dom (CantorNF c) ) by TARSKI:def 3;
i in omega by ORDINAL1:def 12;
then x in omega by A15, ORDINAL1:10;
then reconsider x = x as Nat ;
A16: (CantorNF c) . x = {} by A15, FUNCT_1:def 2;
x in Segm i by A15;
then (CantorNF b) . x = (CantorNF c) . x by A8, NAT_1:44;
then dom (CantorNF b) c= x by A16, FUNCT_1:def 9, ORDINAL1:16;
then dom (CantorNF b) in i by A15, ORDINAL1:12;
then A17: (CantorNF b) . i = {} by FUNCT_1:def 2;
dom (CantorNF c) in i by A14, ORDINAL1:16;
hence contradiction by A8, A17, FUNCT_1:def 2; :: thesis: verum

end;

end;

end;

A18: dom ((CantorNF b) | i) = (dom (CantorNF b)) /\ i by RELAT_1:61
.= i by A9, XBOOLE_1:28
.= (dom (CantorNF c)) /\ i by A9, XBOOLE_1:28
.= dom ((CantorNF c) | i) by RELAT_1:61 ;
for x being object st x in dom ((CantorNF b) | i) holds
((CantorNF b) | i) . x = ((CantorNF c) | i) . x

proof

let x be object ; :: thesis: ( x in dom ((CantorNF b) | i) implies ((CantorNF b) | i) . x = ((CantorNF c) | i) . x )
assume x in dom ((CantorNF b) | i) ; :: thesis: ((CantorNF b) | i) . x = ((CantorNF c) | i) . x
then A19: x in i by RELAT_1:57;
i in omega by ORDINAL1:def 12;
then x in omega by A19, ORDINAL1:10;
then reconsider m = x as Nat ;
m in Segm i by A19;
then A20: m < i by NAT_1:44;
thus ((CantorNF b) | i) . x = (CantorNF b) . m by A19, FUNCT_1:49
.= (CantorNF c) . m by A8, A20
.= ((CantorNF c) | i) . x by A19, FUNCT_1:49 ; :: thesis: verum

end;

then A21: (CantorNF b) | i = (CantorNF c) | i by A18, FUNCT_1:2;
A22: Sum^ ((CantorNF b) /^ i) in Sum^ ((CantorNF c) /^ i)

proof

Sum^ (CantorNF b) in Sum^ (((CantorNF c) | i) ^ ((CantorNF c) /^ i)) by A1;
then Sum^ (((CantorNF b) | i) ^ ((CantorNF b) /^ i)) in (Sum^ ((CantorNF c) | i)) +^ (Sum^ ((CantorNF c) /^ i)) by Th24;
then (Sum^ ((CantorNF b) | i)) +^ (Sum^ ((CantorNF b) /^ i)) in (Sum^ ((CantorNF c) | i)) +^ (Sum^ ((CantorNF c) /^ i)) by Th24;
hence Sum^ ((CantorNF b) /^ i) in Sum^ ((CantorNF c) /^ i) by A21, ORDINAL3:22; :: thesis: verum

end;

A23: ((CantorNF b) | i) ^ ((CantorNF b) /^ i) is Cantor-normal-form ;
A24: ((CantorNF c) | i) ^ ((CantorNF c) /^ i) is Cantor-normal-form ;
A25: b = Sum^ (((CantorNF b) | i) ^ ((CantorNF b) /^ i))
.= (Sum^ ((CantorNF b) | i)) +^ (Sum^ ((CantorNF b) /^ i)) by Th24
.= (Sum^ ((CantorNF b) | i)) (+) (Sum^ ((CantorNF b) /^ i)) by A23, Th84 ;
A26: c = Sum^ (((CantorNF c) | i) ^ ((CantorNF c) /^ i))
.= (Sum^ ((CantorNF c) | i)) +^ (Sum^ ((CantorNF c) /^ i)) by Th24
.= (Sum^ ((CantorNF c) | i)) (+) (Sum^ ((CantorNF c) /^ i)) by A24, Th84 ;
A27: not a (+) (Sum^ ((CantorNF b) | i)) is empty by A2;
((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0

proof

( 0 in dom ((CantorNF b) /^ i) or 0 in dom ((CantorNF c) /^ i) )

proof

assume ( not 0 in dom ((CantorNF b) /^ i) & not 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: contradiction
then ( dom ((CantorNF b) /^ i) c= {} & dom ((CantorNF c) /^ i) c= {} ) by ORDINAL1:16;
then ( (CantorNF b) /^ i = {} & (CantorNF c) /^ i = {} ) ;
then ( ((CantorNF b) | i) ^ ((CantorNF b) /^ i) = (CantorNF b) | i & ((CantorNF c) | i) ^ ((CantorNF c) /^ i) = (CantorNF c) | i ) ;
then A28: ( CantorNF b = (CantorNF b) | i & CantorNF c = (CantorNF c) | i ) ;
not i in i ;
then ( not i in (dom (CantorNF b)) /\ i & not i in (dom (CantorNF c)) /\ i ) by XBOOLE_0:def 4;
then A29: ( not i in dom ((CantorNF b) | i) & not i in dom ((CantorNF c) | i) ) by RELAT_1:61;
then (CantorNF b) . i = {} by A28, FUNCT_1:def 2
.= (CantorNF c) . i by A28, A29, FUNCT_1:def 2 ;
hence contradiction by A8; :: thesis: verum

end;

per cases then ( ( 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) or ( 0 in dom ((CantorNF b) /^ i) & not 0 in dom ((CantorNF c) /^ i) ) or ( not 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) ) ;

suppose ( 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0

then ( ((CantorNF b) /^ i) . 0 = (CantorNF b) . (0 + i) & ((CantorNF c) /^ i) . 0 = (CantorNF c) . (0 + i) ) by AFINSQ_2:def 2;
hence ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0 by A8; :: thesis: verum

end;

suppose ( 0 in dom ((CantorNF b) /^ i) & not 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0

then ( ((CantorNF b) /^ i) . 0 <> {} & ((CantorNF c) /^ i) . 0 = {} ) by FUNCT_1:def 9, FUNCT_1:def 2;
hence ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0 ; :: thesis: verum

end;

suppose ( not 0 in dom ((CantorNF b) /^ i) & 0 in dom ((CantorNF c) /^ i) ) ; :: thesis: ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0

then ( ((CantorNF b) /^ i) . 0 = {} & ((CantorNF c) /^ i) . 0 <> {} ) by FUNCT_1:def 9, FUNCT_1:def 2;
hence ((CantorNF b) /^ i) . 0 <> ((CantorNF c) /^ i) . 0 ; :: thesis: verum

end;

end;

end;

then (CantorNF (Sum^ ((CantorNF b) /^ i))) . 0 <> (CantorNF (Sum^ ((CantorNF c) /^ i))) . 0 ;
then (a (+) (Sum^ ((CantorNF b) | i))) (+) (Sum^ ((CantorNF b) /^ i)) in (a (+) (Sum^ ((CantorNF c) | i))) (+) (Sum^ ((CantorNF c) /^ i)) by A21, A22, A27, Lm11;
then a (+) b in (a (+) (Sum^ ((CantorNF c) | i))) (+) (Sum^ ((CantorNF c) /^ i)) by A25, Th81;
hence a (+) b in a (+) c by A26, Th81; :: thesis: verum

end;

end;