let a, b, c be Ordinal; :: thesis: ( a (+) b = a (+) c implies b = c )
assume A1: a (+) b = a (+) c ; :: thesis: b = c
set C1 = CantorNF (a (+) b);
set C2 = CantorNF (a (+) c);
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set E3 = omega -exponent (CantorNF c);
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
set L3 = omega -leading_coeff (CantorNF c);
A2: rng (omega -exponent (CantorNF b)) = rng (omega -exponent (CantorNF c))

proof

assume rng (omega -exponent (CantorNF b)) <> rng (omega -exponent (CantorNF c)) ; :: thesis: contradiction

per cases then ( not rng (omega -exponent (CantorNF b)) c= rng (omega -exponent (CantorNF c)) or not rng (omega -exponent (CantorNF c)) c= rng (omega -exponent (CantorNF b)) ) by XBOOLE_0:def 10;

suppose not rng (omega -exponent (CantorNF b)) c= rng (omega -exponent (CantorNF c)) ; :: thesis: contradiction

then consider y being object such that
A3: ( y in rng (omega -exponent (CantorNF b)) & not y in rng (omega -exponent (CantorNF c)) ) by TARSKI:def 3;
y in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by A3, XBOOLE_0:def 3;
then A4: y in rng (omega -exponent (CantorNF (a (+) b))) by Th76;
then consider x being object such that
A5: ( x in dom (omega -exponent (CantorNF (a (+) b))) & (omega -exponent (CantorNF (a (+) b))) . x = y ) by FUNCT_1:def 3;
A6: x in dom (CantorNF (a (+) b)) by A5, Def1;
then A7: y = omega -exponent ((CantorNF (a (+) b)) . x) by A5, Def1;
A8: omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF a))

proof

assume not omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF a)) ; :: thesis: contradiction
then not y in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF c))) by A3, A7, XBOOLE_0:def 3;
hence contradiction by A1, A4, Th76; :: thesis: verum

end;

then omega -exponent ((CantorNF (a (+) b)) . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by A3, A7, XBOOLE_0:def 4;
then A9: omega -leading_coeff ((CantorNF (a (+) b)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) by A6, Th80;
omega -exponent ((CantorNF (a (+) b)) . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF c))) by A3, A7, A8, XBOOLE_0:def 5;
then omega -leading_coeff ((CantorNF (a (+) b)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) + 0 by A1, A6, Th78;
then A10: 0 = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . y) by A7, A9;
y in dom ((omega -exponent (CantorNF b)) ") by A3, FUNCT_1:33;
then ((omega -exponent (CantorNF b)) ") . y in rng ((omega -exponent (CantorNF b)) ") by FUNCT_1:3;
then ((omega -exponent (CantorNF b)) ") . y in dom (omega -exponent (CantorNF b)) by FUNCT_1:33;
then ((omega -exponent (CantorNF b)) ") . y in dom (CantorNF b) by Def1;
then ((omega -exponent (CantorNF b)) ") . y in dom (omega -leading_coeff (CantorNF b)) by Def3;
hence contradiction by A10, FUNCT_1:def 9; :: thesis: verum

end;

suppose not rng (omega -exponent (CantorNF c)) c= rng (omega -exponent (CantorNF b)) ; :: thesis: contradiction

then consider y being object such that
A11: ( y in rng (omega -exponent (CantorNF c)) & not y in rng (omega -exponent (CantorNF b)) ) by TARSKI:def 3;
y in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF c))) by A11, XBOOLE_0:def 3;
then A12: y in rng (omega -exponent (CantorNF (a (+) c))) by Th76;
then consider x being object such that
A13: ( x in dom (omega -exponent (CantorNF (a (+) c))) & (omega -exponent (CantorNF (a (+) c))) . x = y ) by FUNCT_1:def 3;
A14: x in dom (CantorNF (a (+) c)) by A13, Def1;
then A15: y = omega -exponent ((CantorNF (a (+) c)) . x) by A13, Def1;
A16: omega -exponent ((CantorNF (a (+) c)) . x) in rng (omega -exponent (CantorNF a))

proof

assume not omega -exponent ((CantorNF (a (+) c)) . x) in rng (omega -exponent (CantorNF a)) ; :: thesis: contradiction
then not y in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by A11, A15, XBOOLE_0:def 3;
hence contradiction by A1, A12, Th76; :: thesis: verum

end;

then omega -exponent ((CantorNF (a (+) c)) . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF c))) by A11, A15, XBOOLE_0:def 4;
then A17: omega -leading_coeff ((CantorNF (a (+) c)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) c)) . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent ((CantorNF (a (+) c)) . x)))) by A14, Th80;
omega -exponent ((CantorNF (a (+) c)) . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by A11, A15, A16, XBOOLE_0:def 5;
then omega -leading_coeff ((CantorNF (a (+) c)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) c)) . x)))) + 0 by A1, A14, Th78;
then A18: 0 = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . y) by A15, A17;
y in dom ((omega -exponent (CantorNF c)) ") by A11, FUNCT_1:33;
then ((omega -exponent (CantorNF c)) ") . y in rng ((omega -exponent (CantorNF c)) ") by FUNCT_1:3;
then ((omega -exponent (CantorNF c)) ") . y in dom (omega -exponent (CantorNF c)) by FUNCT_1:33;
then ((omega -exponent (CantorNF c)) ") . y in dom (CantorNF c) by Def1;
then ((omega -exponent (CantorNF c)) ") . y in dom (omega -leading_coeff (CantorNF c)) by Def3;
hence contradiction by A18, FUNCT_1:def 9; :: thesis: verum

end;

end;

end;

then A19: omega -exponent (CantorNF b) = omega -exponent (CantorNF c) by Th34;
A20: dom (omega -leading_coeff (CantorNF b)) = dom (CantorNF b) by Def3
.= card (dom (omega -exponent (CantorNF b))) by Def1
.= card (rng (omega -exponent (CantorNF b))) by CARD_1:70
.= card (dom (omega -exponent (CantorNF c))) by A2, CARD_1:70
.= dom (CantorNF c) by Def1
.= dom (omega -leading_coeff (CantorNF c)) by Def3 ;
for x being object st x in dom (omega -leading_coeff (CantorNF b)) holds
(omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x

proof

let x be object ; :: thesis: ( x in dom (omega -leading_coeff (CantorNF b)) implies (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x )
assume x in dom (omega -leading_coeff (CantorNF b)) ; :: thesis: (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x
then x in dom (CantorNF b) by Def3;
then A21: x in dom (omega -exponent (CantorNF b)) by Def1;
then A22: (omega -exponent (CantorNF b)) . x in rng (omega -exponent (CantorNF b)) by FUNCT_1:3;
then (omega -exponent (CantorNF b)) . x in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 3;
then (omega -exponent (CantorNF b)) . x in rng (omega -exponent (CantorNF (a (+) b))) by Th76;
then consider y being object such that
A23: ( y in dom (omega -exponent (CantorNF (a (+) b))) & (omega -exponent (CantorNF (a (+) b))) . y = (omega -exponent (CantorNF b)) . x ) by FUNCT_1:def 3;
A24: y in dom (CantorNF (a (+) b)) by A23, Def1;
then A25: omega -exponent ((CantorNF (a (+) b)) . y) = (omega -exponent (CantorNF b)) . x by A23, Def1;

per cases ( omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a)) or not omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a)) ) ;

suppose omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a)) ; :: thesis: (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x

then A26: omega -exponent ((CantorNF (a (+) b)) . y) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by A22, A25, XBOOLE_0:def 4;
then A27: omega -exponent ((CantorNF (a (+) c)) . y) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF c))) by A1, A2;
((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF b)) . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . x))) = omega -leading_coeff ((CantorNF (a (+) b)) . y) by A24, A25, A26, Th80
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF b)) . x))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . ((omega -exponent (CantorNF b)) . x))) by A1, A24, A25, A27, Th80 ;
hence (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . ((omega -exponent (CantorNF b)) . x)) by A21, FUNCT_1:34
.= (omega -leading_coeff (CantorNF c)) . x by A19, A21, FUNCT_1:34 ;
:: thesis: verum

end;

suppose not omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a)) ; :: thesis: (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x

then A29: omega -exponent ((CantorNF (a (+) b)) . y) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) by A22, A25, XBOOLE_0:def 5;
then A30: omega -exponent ((CantorNF (a (+) c)) . y) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF a))) by A1, A2;
thus (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . x)) by A21, FUNCT_1:34
.= omega -leading_coeff ((CantorNF (a (+) b)) . y) by A24, A25, A29, Th79
.= (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . ((omega -exponent (CantorNF b)) . x)) by A1, A24, A25, A30, Th79
.= (omega -leading_coeff (CantorNF c)) . x by A19, A21, FUNCT_1:34 ; :: thesis: verum

end;

end;

end;

then omega -leading_coeff (CantorNF b) = omega -leading_coeff (CantorNF c) by A20, FUNCT_1:2;
then Sum^ (CantorNF b) = Sum^ (CantorNF c) by A19, Th67;
hence b = c ; :: thesis: verum