let a be Ordinal; :: thesis: a (+) 0 = a
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF 0);
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF 0);
consider C being Cantor-normal-form Ordinal-Sequence such that
A1: ( a (+) 0 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF 0))) ) and
A2: for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF 0))) 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 0))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF 0)) . (((omega -exponent (CantorNF 0)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF 0))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF 0)) . (((omega -exponent (CantorNF 0)) ") . (omega -exponent (C . d)))) ) ) by Def5;
A3: rng (omega -exponent (CantorNF 0)) is empty ;
then A4: rng (omega -exponent C) = rng (omega -exponent (CantorNF a)) by A1;
A5: dom C = card (dom (omega -exponent C)) by Def1
.= card (rng (omega -exponent C)) by CARD_1:70
.= card (dom (omega -exponent (CantorNF a))) by A4, CARD_1:70
.= dom (CantorNF a) by Def1 ;
for x being object st x in dom C holds
C . x = (CantorNF a) . x then C = CantorNF a by A5, FUNCT_1:2;
hence a (+) 0 = a by A1; :: thesis: verum