let a, b be Ordinal; :: thesis: ( rng (omega -exponent (CantorNF a)) = rng (omega -exponent (CantorNF b)) implies for c being Ordinal st c in dom (CantorNF a) holds
(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c) )
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);
assume A1: rng (omega -exponent (CantorNF a)) = rng (omega -exponent (CantorNF b)) ; :: thesis: for c being Ordinal st c in dom (CantorNF a) holds
(omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)
then A2: omega -exponent (CantorNF a) = omega -exponent (CantorNF b) by Th34;
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;
let c be Ordinal; :: thesis: ( c in dom (CantorNF a) implies (omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c) )
assume A5: c in dom (CantorNF a) ; :: thesis: (omega -leading_coeff (CantorNF (a (+) b))) . c = ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c)
A6: dom (CantorNF a) = card (dom (omega -exponent (CantorNF a))) by Def1
.= card (rng (omega -exponent (CantorNF a))) by CARD_1:70
.= card (dom (omega -exponent C)) by A1, A3, CARD_1:70
.= dom C by Def1 ;
A7: rng (omega -exponent C) = rng (omega -exponent (CantorNF a)) by A1, A3;
then A8: rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by A1;
c in dom (omega -exponent C) by A5, A6, Def1;
then (omega -exponent C) . c in rng (omega -exponent C) by FUNCT_1:3;
then A9: omega -exponent (C . c) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by A5, A6, A8, Def1;
A10: omega -exponent C = omega -exponent (CantorNF a) by A7, Th34;
A11: c in dom (omega -exponent (CantorNF a)) by A5, Def1;
thus (omega -leading_coeff (CantorNF (a (+) b))) . c = omega -leading_coeff (C . c) by A3, A5, A6, Def3
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . c)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . c)))) by A4, A5, A6, A9
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . c))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . c)))) by A5, A6, A10, Def1
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . c))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . c))) by A2, A5, A6, A10, Def1
.= ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . c))) by A11, FUNCT_1:34
.= ((omega -leading_coeff (CantorNF a)) . c) + ((omega -leading_coeff (CantorNF b)) . c) by A2, A11, FUNCT_1:34 ; :: thesis: verum