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

proof

let x be object ; :: thesis: ( x in dom C implies C . x = (CantorNF a) . x )
A6: omega -exponent C = omega -exponent (CantorNF a) by A4, Th34;
assume A7: x in dom C ; :: thesis: C . x = (CantorNF a) . x
then A8: x in dom (omega -exponent C) by Def1;
then (omega -exponent C) . x in rng (omega -exponent (CantorNF a)) by A4, FUNCT_1:3;
then omega -exponent (C . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF 0))) by A3, A7, Def1;
then A9: omega -leading_coeff (C . x) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . x))) by A2, A7
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent C) . x)) by A7, Def1
.= (omega -leading_coeff (CantorNF a)) . x by A6, A8, FUNCT_1:34 ;
A10: x in dom (CantorNF a) by A6, A8, Def1;
thus C . x = ((omega -leading_coeff (CantorNF a)) . x) *^ (exp (omega,(omega -exponent (C . x)))) by A7, A9, Th64
.= ((omega -leading_coeff (CantorNF a)) . x) *^ (exp (omega,((omega -exponent (CantorNF a)) . x))) by A6, A7, Def1
.= ((omega -leading_coeff (CantorNF a)) . x) *^ (exp (omega,(omega -exponent ((CantorNF a) . x)))) by A10, Def1
.= (omega -leading_coeff ((CantorNF a) . x)) *^ (exp (omega,(omega -exponent ((CantorNF a) . x)))) by A10, Def3
.= (CantorNF a) . x by A10, Th64 ; :: thesis: verum

end;

then C = CantorNF a by A5, FUNCT_1:2;
hence a (+) 0 = a by A1; :: thesis: verum