let a, b be Ordinal; :: thesis: ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
set C0 = CantorNF (a (+) b);

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

suppose A1: a (+) b <> {} ; :: thesis: ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )

then 0 c< dom (CantorNF (a (+) b)) by XBOOLE_1:2, XBOOLE_0:def 8;
then A2: 0 in dom (CantorNF (a (+) b)) by ORDINAL1:11;
consider C being Cantor-normal-form Ordinal-Sequence such that
A3: ( a (+) b = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) ) and
A4: for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) by Def5;
C <> {} by A1, A3, ORDINAL5:52;
then 0 c< dom C by XBOOLE_1:2, XBOOLE_0:def 8;
then A5: 0 in dom C by ORDINAL1:11;

hereby :: thesis: ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )

assume A6: omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) ; :: thesis: (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0
then omega -exponent (CantorNF a) <> {} ;
then 0 c< dom (omega -exponent (CantorNF a)) by XBOOLE_1:2, XBOOLE_0:def 8;
then A7: 0 in dom (omega -exponent (CantorNF a)) by ORDINAL1:11;
A8: omega -leading_coeff (C . 0) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . 0))) by A3, A4, A5, A6
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . 0)) by A3, A6, Th95
.= (omega -leading_coeff (CantorNF a)) . 0 by A7, FUNCT_1:34 ;
A9: 0 in dom (CantorNF a) by A7, Def1;
thus (CantorNF (a (+) b)) . 0 = (omega -leading_coeff ((CantorNF (a (+) b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0)))) by A2, Th64
.= ((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0))) by A3, A6, A8, Th95
.= (CantorNF a) . 0 by A9, Th65 ; :: thesis: verum

end;

hereby :: thesis: ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) )

assume A10: omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) ; :: thesis: (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0
then omega -exponent (CantorNF b) <> {} ;
then 0 c< dom (omega -exponent (CantorNF b)) by XBOOLE_1:2, XBOOLE_0:def 8;
then A11: 0 in dom (omega -exponent (CantorNF b)) by ORDINAL1:11;
A12: omega -leading_coeff (C . 0) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . 0))) by A3, A4, A5, A10
.= (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . 0)) by A3, A10, Th95
.= (omega -leading_coeff (CantorNF b)) . 0 by A11, FUNCT_1:34 ;
A13: 0 in dom (CantorNF b) by A11, Def1;
thus (CantorNF (a (+) b)) . 0 = (omega -leading_coeff ((CantorNF (a (+) b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0)))) by A2, Th64
.= ((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0))) by A3, A10, A12, Th95
.= (CantorNF b) . 0 by A13, Th65 ; :: thesis: verum

end;

assume A14: omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) ; :: thesis: (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0)
then A15: ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) & omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) ) by XBOOLE_0:def 4;
then ( omega -exponent (CantorNF a) <> {} & omega -exponent (CantorNF b) <> {} ) ;
then ( 0 c< dom (omega -exponent (CantorNF a)) & 0 c< dom (omega -exponent (CantorNF b)) ) by XBOOLE_1:2, XBOOLE_0:def 8;
then A16: ( 0 in dom (omega -exponent (CantorNF a)) & 0 in dom (omega -exponent (CantorNF b)) ) by ORDINAL1:11;
A17: omega -leading_coeff (C . 0) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . 0)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . 0)))) by A3, A4, A5, A14
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . 0))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . 0)))) by A3, A15, Th95
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . 0))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . 0))) by A15, Th95
.= ((omega -leading_coeff (CantorNF a)) . 0) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . 0))) by A16, FUNCT_1:34
.= ((omega -leading_coeff (CantorNF a)) . 0) + ((omega -leading_coeff (CantorNF b)) . 0) by A16, FUNCT_1:34 ;
A18: ( 0 in dom (CantorNF a) & 0 in dom (CantorNF b) ) by A16, Def1;
thus (CantorNF (a (+) b)) . 0 = (omega -leading_coeff ((CantorNF (a (+) b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0)))) by A2, Th64
.= (((omega -leading_coeff (CantorNF a)) . 0) +^ ((omega -leading_coeff (CantorNF b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0)))) by A3, A17, CARD_2:36
.= (((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))) by ORDINAL3:46
.= (((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0)))) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))) by A15, Th95
.= (((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0)))) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0)))) by A15, Th95
.= ((CantorNF a) . 0) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0)))) by A18, Th65
.= ((CantorNF a) . 0) +^ ((CantorNF b) . 0) by A18, Th65 ; :: thesis: verum

end;

suppose a (+) b = {} ; :: thesis: ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )

then ( a = {} & b = {} ) ;
hence ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) ) ; :: thesis: verum

end;

end;