let a, b be Ordinal; :: thesis: for d being object st d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) holds
omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))
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);
consider C being Cantor-normal-form Ordinal-Sequence such that
A1: ( a (+) b = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) ) 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 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 d be object ; :: thesis: ( d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) )
assume ( d in dom (CantorNF (a (+) b)) & omega -exponent ((CantorNF (a (+) b)) . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) ) ; :: thesis: omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d)))
hence omega -leading_coeff ((CantorNF (a (+) b)) . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . d))) by A1, A2; :: thesis: verum