let a, b be Ordinal; ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )
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);
set C0 = CantorNF (a (+) b);
per cases
( a (+) b <> {} or a (+) b = {} )
;
suppose A1:
a (+) b <> {}
;
( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = (CantorNF a) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )then
0 c< dom (CantorNF (a (+) b))
by XBOOLE_1:2, XBOOLE_0:def 8;
then A2:
0 in dom (CantorNF (a (+) b))
by ORDINAL1:11;
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;
C <> {}
by A1, A3, ORDINAL5:52;
then
0 c< dom C
by XBOOLE_1:2, XBOOLE_0:def 8;
then A5:
0 in dom C
by ORDINAL1:11;
hereby ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies (CantorNF (a (+) b)) . 0 = (CantorNF b) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) ) )
assume A6:
omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b)))
;
(CantorNF (a (+) b)) . 0 = (CantorNF a) . 0then
omega -exponent (CantorNF a) <> {}
;
then
0 c< dom (omega -exponent (CantorNF a))
by XBOOLE_1:2, XBOOLE_0:def 8;
then A7:
0 in dom (omega -exponent (CantorNF a))
by ORDINAL1:11;
A8:
omega -leading_coeff (C . 0) =
(omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . 0)))
by A3, A4, A5, A6
.=
(omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . 0))
by A3, A6, Th95
.=
(omega -leading_coeff (CantorNF a)) . 0
by A7, FUNCT_1:34
;
A9:
0 in dom (CantorNF a)
by A7, Def1;
thus (CantorNF (a (+) b)) . 0 =
(omega -leading_coeff ((CantorNF (a (+) b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))
by A2, Th64
.=
((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0)))
by A3, A6, A8, Th95
.=
(CantorNF a) . 0
by A9, Th65
;
verum
end; hereby ( omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies (CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0) )
assume A10:
omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a)))
;
(CantorNF (a (+) b)) . 0 = (CantorNF b) . 0then
omega -exponent (CantorNF b) <> {}
;
then
0 c< dom (omega -exponent (CantorNF b))
by XBOOLE_1:2, XBOOLE_0:def 8;
then A11:
0 in dom (omega -exponent (CantorNF b))
by ORDINAL1:11;
A12:
omega -leading_coeff (C . 0) =
(omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . 0)))
by A3, A4, A5, A10
.=
(omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . 0))
by A3, A10, Th95
.=
(omega -leading_coeff (CantorNF b)) . 0
by A11, FUNCT_1:34
;
A13:
0 in dom (CantorNF b)
by A11, Def1;
thus (CantorNF (a (+) b)) . 0 =
(omega -leading_coeff ((CantorNF (a (+) b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))
by A2, Th64
.=
((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0)))
by A3, A10, A12, Th95
.=
(CantorNF b) . 0
by A13, Th65
;
verum
end; assume A14:
omega -exponent ((CantorNF (a (+) b)) . 0) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b)))
;
(CantorNF (a (+) b)) . 0 = ((CantorNF a) . 0) +^ ((CantorNF b) . 0)then A15:
(
omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) &
omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) )
by XBOOLE_0:def 4;
then
(
omega -exponent (CantorNF a) <> {} &
omega -exponent (CantorNF b) <> {} )
;
then
(
0 c< dom (omega -exponent (CantorNF a)) &
0 c< dom (omega -exponent (CantorNF b)) )
by XBOOLE_1:2, XBOOLE_0:def 8;
then A16:
(
0 in dom (omega -exponent (CantorNF a)) &
0 in dom (omega -exponent (CantorNF b)) )
by ORDINAL1:11;
A17:
omega -leading_coeff (C . 0) =
((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . 0)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . 0))))
by A3, A4, A5, A14
.=
((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . 0))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . 0))))
by A3, A15, Th95
.=
((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . 0))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . 0)))
by A15, Th95
.=
((omega -leading_coeff (CantorNF a)) . 0) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . 0)))
by A16, FUNCT_1:34
.=
((omega -leading_coeff (CantorNF a)) . 0) + ((omega -leading_coeff (CantorNF b)) . 0)
by A16, FUNCT_1:34
;
A18:
(
0 in dom (CantorNF a) &
0 in dom (CantorNF b) )
by A16, Def1;
thus (CantorNF (a (+) b)) . 0 =
(omega -leading_coeff ((CantorNF (a (+) b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))
by A2, Th64
.=
(((omega -leading_coeff (CantorNF a)) . 0) +^ ((omega -leading_coeff (CantorNF b)) . 0)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))
by A3, A17, CARD_2:36
.=
(((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0))))) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0)))))
by ORDINAL3:46
.=
(((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0)))) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . 0)))))
by A15, Th95
.=
(((omega -leading_coeff (CantorNF a)) . 0) *^ (exp (omega,((omega -exponent (CantorNF a)) . 0)))) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0))))
by A15, Th95
.=
((CantorNF a) . 0) +^ (((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0))))
by A18, Th65
.=
((CantorNF a) . 0) +^ ((CantorNF b) . 0)
by A18, Th65
;
verum end;