let a, b, c be Ordinal; :: thesis: (a (+) b) (+) c = a (+) (b (+) c)
set s4 = a (+) b;
set s5 = b (+) c;
set s6 = (a (+) b) (+) c;
set s7 = a (+) (b (+) c);
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set E3 = omega -exponent (CantorNF c);
set E4 = omega -exponent (CantorNF (a (+) b));
set E5 = omega -exponent (CantorNF (b (+) c));
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
set L3 = omega -leading_coeff (CantorNF c);
set L4 = omega -leading_coeff (CantorNF (a (+) b));
set L5 = omega -leading_coeff (CantorNF (b (+) c));
consider C4 being Cantor-normal-form Ordinal-Sequence such that
A1: ( a (+) b = Sum^ C4 & rng (omega -exponent C4) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) ) and
A2: for d being object st d in dom C4 holds
( ( omega -exponent (C4 . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C4 . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C4 . d))) ) & ( omega -exponent (C4 . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C4 . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C4 . d))) ) & ( omega -exponent (C4 . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C4 . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C4 . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C4 . d)))) ) ) by Def5;
consider C5 being Cantor-normal-form Ordinal-Sequence such that
A3: ( b (+) c = Sum^ C5 & rng (omega -exponent C5) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF c))) ) and
A4: for d being object st d in dom C5 holds
( ( omega -exponent (C5 . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C5 . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C5 . d))) ) & ( omega -exponent (C5 . d) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C5 . d) = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C5 . d))) ) & ( omega -exponent (C5 . d) in (rng (omega -exponent (CantorNF b))) /\ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C5 . d) = ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C5 . d)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C5 . d)))) ) ) by Def5;
consider C6 being Cantor-normal-form Ordinal-Sequence such that
A5: ( (a (+) b) (+) c = Sum^ C6 & rng (omega -exponent C6) = (rng (omega -exponent (CantorNF (a (+) b)))) \/ (rng (omega -exponent (CantorNF c))) ) and
A6: for d being object st d in dom C6 holds
( ( omega -exponent (C6 . d) in (rng (omega -exponent (CantorNF (a (+) b)))) \ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C6 . d) = (omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . d))) ) & ( omega -exponent (C6 . d) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF (a (+) b)))) implies omega -leading_coeff (C6 . d) = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . d))) ) & ( omega -exponent (C6 . d) in (rng (omega -exponent (CantorNF (a (+) b)))) /\ (rng (omega -exponent (CantorNF c))) implies omega -leading_coeff (C6 . d) = ((omega -leading_coeff (CantorNF (a (+) b))) . (((omega -exponent (CantorNF (a (+) b))) ") . (omega -exponent (C6 . d)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent (C6 . d)))) ) ) by Def5;
consider C7 being Cantor-normal-form Ordinal-Sequence such that
A7: ( a (+) (b (+) c) = Sum^ C7 & rng (omega -exponent C7) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF (b (+) c)))) ) and
A8: for d being object st d in dom C7 holds
( ( omega -exponent (C7 . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF (b (+) c)))) implies omega -leading_coeff (C7 . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C7 . d))) ) & ( omega -exponent (C7 . d) in (rng (omega -exponent (CantorNF (b (+) c)))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C7 . d) = (omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . d))) ) & ( omega -exponent (C7 . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF (b (+) c)))) implies omega -leading_coeff (C7 . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C7 . d)))) + ((omega -leading_coeff (CantorNF (b (+) c))) . (((omega -exponent (CantorNF (b (+) c))) ") . (omega -exponent (C7 . d)))) ) ) by Def5;
A9: rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by A1;
A10: rng (omega -exponent (CantorNF (b (+) c))) = (rng (omega -exponent (CantorNF b))) \/ (rng (omega -exponent (CantorNF c))) by A3;
A11: omega -exponent C6 = omega -exponent C7 by A1, A3, A5, A7, Th34, XBOOLE_1:4;
A12: dom C6 = dom (omega -exponent C6) by Def1
.= dom C7 by A11, Def1 ;
for x being object st x in dom C6 holds
C6 . x = C7 . x hence (a (+) b) (+) c = a (+) (b (+) c) by A5, A7, A12, FUNCT_1:2; :: thesis: verum