let a, b, c be Ordinal; :: thesis: (a (+) b) (+) c = a (+) (b (+) c)
set s4 = a (+) b;
set s5 = b (+) c;
set s6 = (a (+) b) (+) c;
set s7 = a (+) (b (+) c);
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set E3 = omega -exponent (CantorNF c);
set E4 = omega -exponent (CantorNF (a (+) b));
set E5 = omega -exponent (CantorNF (b (+) c));
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
set L3 = omega -leading_coeff (CantorNF c);
set L4 = omega -leading_coeff (CantorNF (a (+) b));
set L5 = omega -leading_coeff (CantorNF (b (+) c));
consider C4 being Cantor-normal-form Ordinal-Sequence such that
A1: ( a (+) b = Sum^ C4 & rng (omega -exponent C4) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) ) and
A2: for d being object st d in dom C4 holds
( ( omega -exponent (C4 . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C4 . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C4 . d))) ) & ( omega -exponent (C4 . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C4 . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C4 . d))) ) & ( omega -exponent (C4 . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C4 . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C4 . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C4 . d)))) ) ) by Def5;
consider C5 being Cantor-normal-form Ordinal-Sequence such that
A3: ( b (+) c = Sum^ C5 & rng (omega -exponent C5) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF c))) ) and
A4: for d being object st d in dom C5 holds
( ( omega -exponent (C5 . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C5 . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C5 . d))) ) & ( omega -exponent (C5 . d) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C5 . d) = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C5 . d))) ) & ( omega -exponent (C5 . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C5 . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C5 . d)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C5 . d)))) ) ) by Def5;
consider C6 being Cantor-normal-form Ordinal-Sequence such that
A5: ( (a (+) b) (+) c = Sum^ C6 & rng (omega -exponent C6) = (rng (omega -exponent (CantorNF (a (+) b)))) \/ (rng (omega -exponent (CantorNF c))) ) and
A6: for d being object st d in dom C6 holds
( ( omega -exponent (C6 . d) in (rng (omega -exponent (CantorNF (a (+) b)))) \ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C6 . d) = (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . d))) ) & ( omega -exponent (C6 . d) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF (a (+) b)))) implies omega -leading_coeff (C6 . d) = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . d))) ) & ( omega -exponent (C6 . d) in (rng (omega -exponent (CantorNF (a (+) b)))) /\ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C6 . d) = ((omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . d)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . d)))) ) ) by Def5;
consider C7 being Cantor-normal-form Ordinal-Sequence such that
A7: ( a (+) (b (+) c) = Sum^ C7 & rng (omega -exponent C7) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF (b (+) c)))) ) and
A8: for d being object st d in dom C7 holds
( ( omega -exponent (C7 . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF (b (+) c)))) implies omega -leading_coeff (C7 . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C7 . d))) ) & ( omega -exponent (C7 . d) in (rng (omega -exponent (CantorNF (b (+) c)))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C7 . d) = (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . d))) ) & ( omega -exponent (C7 . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF (b (+) c)))) implies omega -leading_coeff (C7 . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C7 . d)))) + ((omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . d)))) ) ) by Def5;
A9: rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by A1;
A10: rng (omega -exponent (CantorNF (b (+) c))) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF c))) by A3;
A11: omega -exponent C6 = omega -exponent C7 by A1, A3, A5, A7, Th34, XBOOLE_1:4;
A12: dom C6 = dom (omega -exponent C6) by Def1
.= dom C7 by A11, Def1 ;
for x being object st x in dom C6 holds
C6 . x = C7 . x

proof

let x be object ; :: thesis: ( x in dom C6 implies C6 . x = C7 . x )
assume A13: x in dom C6 ; :: thesis: C6 . x = C7 . x
then A14: ( x in dom (omega -exponent C6) & x in dom C7 ) by A12, Def1;
A15: ( rng (omega -exponent (CantorNF a)) c= rng (omega -exponent (CantorNF (a (+) b))) & rng (omega -exponent (CantorNF b)) c= rng (omega -exponent (CantorNF (a (+) b))) & rng (omega -exponent (CantorNF b)) c= rng (omega -exponent (CantorNF (b (+) c))) & rng (omega -exponent (CantorNF c)) c= rng (omega -exponent (CantorNF (b (+) c))) ) by A1, A3, XBOOLE_1:7;
set e = omega -exponent (C6 . x);
set x1 = ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x));
set y1 = ((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . x));
set x2 = ((omega -exponent (CantorNF a)) ") . (omega -exponent (C7 . x));
set y2 = ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x));
A16: omega -exponent (C6 . x) = (omega -exponent C6) . x by A13, Def1;
then A17: omega -exponent (C6 . x) = omega -exponent (C7 . x) by A11, A14, Def1;
A18: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) implies ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) )

proof

assume A19: omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) ; :: thesis: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) )
then omega -exponent (C6 . x) in dom ((omega -exponent (CantorNF (a (+) b))) ") by FUNCT_1:33;
then ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in rng ((omega -exponent (CantorNF (a (+) b))) ") by FUNCT_1:3;
then ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom (omega -exponent (CantorNF (a (+) b))) by FUNCT_1:33;
hence ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 by A1, Def1; :: thesis: omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x)
hence omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = (omega -exponent (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) by A1, Def1
.= omega -exponent (C6 . x) by A19, FUNCT_1:35 ;
:: thesis: verum

end;

A20: ( omega -exponent (C7 . x) in rng (omega -exponent (CantorNF (b (+) c))) implies ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) )

proof

assume A21: omega -exponent (C7 . x) in rng (omega -exponent (CantorNF (b (+) c))) ; :: thesis: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) )
then omega -exponent (C7 . x) in dom ((omega -exponent (CantorNF (b (+) c))) ") by FUNCT_1:33;
then ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in rng ((omega -exponent (CantorNF (b (+) c))) ") by FUNCT_1:3;
then ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom (omega -exponent (CantorNF (b (+) c))) by FUNCT_1:33;
hence ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 by A3, Def1; :: thesis: omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x)
hence omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = (omega -exponent (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) by A3, Def1
.= omega -exponent (C7 . x) by A21, FUNCT_1:35 ;
:: thesis: verum

end;

omega -exponent (C6 . x) in rng (omega -exponent C6) by A14, A16, FUNCT_1:3;
then ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) or omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) by A1, A5, XBOOLE_0:def 3;

per cases then ( ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) or ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) or ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) or ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) or ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) or ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) or ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ) by XBOOLE_0:def 3;

suppose A22: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A23: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF c))) ) by XBOOLE_0:def 4;
A24: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A15, A22;
then A25: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (a (+) b)))) /\ (rng (omega -exponent (CantorNF c))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF (b (+) c)))) ) by A22, XBOOLE_0:def 4;
A26: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) by A18, A24;
then A27: (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) = omega -leading_coeff (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) by A1, Def3
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C6 . x)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C6 . x)))) by A2, A23, A26 ;
A28: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) by A17, A20, A24;
then A29: (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) = omega -leading_coeff (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A3, Def3
.= ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C7 . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C7 . x)))) by A4, A17, A23, A28 ;
omega -leading_coeff (C6 . x) = ((omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . x)))) by A6, A13, A25
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C6 . x)))) + ((omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A17, A27, A29
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A25 ;
hence C6 . x = (omega -leading_coeff (C7 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, Th64 ;
:: thesis: verum

end;

suppose A31: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A32: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF c))) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;
A33: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A15, A31;
then A34: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (a (+) b)))) \ (rng (omega -exponent (CantorNF c))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF (b (+) c)))) ) by A31, XBOOLE_0:def 4, XBOOLE_0:def 5;
A35: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) by A18, A33;
then A36: (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) = omega -leading_coeff (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) by A1, Def3
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C6 . x)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C6 . x)))) by A2, A32, A35 ;
A37: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) by A17, A20, A33;
then A38: (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) = omega -leading_coeff (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A3, Def3
.= (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C7 . x))) by A4, A17, A32, A37 ;
omega -leading_coeff (C6 . x) = (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) by A6, A13, A34
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A34, A36, A38 ;
hence C6 . x = (omega -leading_coeff (C7 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, Th64 ;
:: thesis: verum

end;

suppose A40: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A41: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF b))) ) by XBOOLE_0:def 5;
A42: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A15, A40;
then A43: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (a (+) b)))) /\ (rng (omega -exponent (CantorNF c))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF (b (+) c)))) ) by A40, XBOOLE_0:def 4;
A44: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) by A18, A42;
then A45: (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) = omega -leading_coeff (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) by A1, Def3
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C6 . x))) by A2, A41, A44 ;
A46: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) by A17, A20, A42;
then A47: (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) = omega -leading_coeff (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A3, Def3
.= (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C7 . x))) by A4, A17, A41, A46 ;
omega -leading_coeff (C6 . x) = ((omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . x)))) by A6, A13, A43
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A43, A45, A47 ;
hence C6 . x = (omega -leading_coeff (C7 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, Th64 ;
:: thesis: verum

end;

suppose A49: ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A50: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF c))) ) by XBOOLE_0:def 4, XBOOLE_0:def 5;
A51: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A15, A49;
then A52: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (a (+) b)))) /\ (rng (omega -exponent (CantorNF c))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (b (+) c)))) \ (rng (omega -exponent (CantorNF a))) ) by A49, XBOOLE_0:def 4, XBOOLE_0:def 5;
A53: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) by A18, A51;
then A54: (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) = omega -leading_coeff (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) by A1, Def3
.= (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C6 . x))) by A2, A50, A53 ;
A55: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) by A17, A20, A51;
then A56: (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) = omega -leading_coeff (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A3, Def3
.= ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C7 . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C7 . x)))) by A4, A17, A50, A55 ;
A57: omega -leading_coeff (C6 . x) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C6 . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . x)))) by A6, A13, A52, A54
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A52, A56 ;
thus C6 . x = (omega -leading_coeff (C6 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, A57, Th64 ; :: thesis: verum

end;

suppose A58: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A59: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) & not omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF c))) ) by XBOOLE_0:def 3, XBOOLE_0:def 5;
then A60: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A10, A15, TARSKI:def 3;
then A61: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (a (+) b)))) \ (rng (omega -exponent (CantorNF c))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF (b (+) c)))) ) by A58, XBOOLE_0:def 5;
A62: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) by A18, A60;
then A63: (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) = omega -leading_coeff (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) by A1, Def3
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C6 . x))) by A2, A59, A62 ;
omega -leading_coeff (C6 . x) = (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) by A6, A13, A61
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A61, A63 ;
hence C6 . x = (omega -leading_coeff (C7 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, Th64 ;
:: thesis: verum

end;

suppose A65: ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A66: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF c))) ) by XBOOLE_0:def 5;
A67: ( omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A15, A65;
then A68: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (a (+) b)))) \ (rng (omega -exponent (CantorNF c))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (b (+) c)))) \ (rng (omega -exponent (CantorNF a))) ) by A65, XBOOLE_0:def 5;
A69: ( ((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)) in dom C4 & omega -exponent (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) = omega -exponent (C6 . x) ) by A18, A67;
then A70: (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x))) = omega -leading_coeff (C4 . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . x)))) by A1, Def3
.= (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C6 . x))) by A2, A66, A69 ;
A71: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) by A17, A20, A67;
then A72: (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) = omega -leading_coeff (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A3, Def3
.= (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C7 . x))) by A4, A17, A66, A71 ;
omega -leading_coeff (C6 . x) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C6 . x))) by A6, A13, A68, A70
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A68, A72 ;
hence C6 . x = (omega -leading_coeff (C7 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, Th64 ;
:: thesis: verum

end;

suppose A74: ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF b)) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF c)) ) ; :: thesis: C6 . x = C7 . x

then A75: ( not omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF b))) ) by XBOOLE_0:def 3, XBOOLE_0:def 5;
then A76: ( not omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (a (+) b))) & omega -exponent (C6 . x) in rng (omega -exponent (CantorNF (b (+) c))) ) by A9, A15, TARSKI:def 3;
then A77: ( omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF (a (+) b)))) & omega -exponent (C6 . x) in (rng (omega -exponent (CantorNF (b (+) c)))) \ (rng (omega -exponent (CantorNF a))) ) by A74, XBOOLE_0:def 5;
A78: ( ((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)) in dom C5 & omega -exponent (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) = omega -exponent (C7 . x) ) by A17, A20, A76;
then A79: (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x))) = omega -leading_coeff (C5 . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . x)))) by A3, Def3
.= (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C7 . x))) by A4, A17, A75, A78 ;
omega -leading_coeff (C6 . x) = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . x))) by A6, A13, A77
.= omega -leading_coeff (C7 . x) by A8, A14, A17, A77, A79 ;
hence C6 . x = (omega -leading_coeff (C7 . x)) *^ (exp (omega,(omega -exponent (C6 . x)))) by A13, Th64
.= C7 . x by A14, A17, Th64 ;
:: thesis: verum

end;

end;

end;

hence (a (+) b) (+) c = a (+) (b (+) c) by A5, A7, A12, FUNCT_1:2; :: thesis: verum