let a, b be Ordinal; :: thesis: for x being object holds (CantorNF a) . x c= (CantorNF (a (+) b)) . x
let x be object ; :: thesis: (CantorNF a) . x c= (CantorNF (a (+) b)) . x
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);
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;
assume not (CantorNF a) . x c= (CantorNF (a (+) b)) . x ; :: thesis: contradiction
then A3: (CantorNF (a (+) b)) . x in (CantorNF a) . x by ORDINAL1:16;
then A4: x in dom (CantorNF a) by FUNCT_1:def 2;
then reconsider x = x as Ordinal ;
dom (CantorNF a) c= dom (CantorNF (a (+) b)) by Th77;
then A5: x in dom (CantorNF (a (+) b)) by A4;
then A6: (CantorNF (a (+) b)) . x = ((omega -leading_coeff (CantorNF (a (+) b))) . x) *^ (exp (omega,((omega -exponent (CantorNF (a (+) b))) . x))) by Th65;
A7: (CantorNF a) . x = ((omega -leading_coeff (CantorNF a)) . x) *^ (exp (omega,((omega -exponent (CantorNF a)) . x))) by A4, Th65;
A8: (omega -exponent (CantorNF a)) . x = (omega -exponent (CantorNF (a (+) b))) . x
proof
A9: (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x by Th97;
assume (omega -exponent (CantorNF a)) . x <> (omega -exponent (CantorNF (a (+) b))) . x ; :: thesis: contradiction
then (omega -exponent (CantorNF a)) . x in (omega -exponent (CantorNF (a (+) b))) . x by A9, XBOOLE_0:def 8, ORDINAL1:11;
then exp (omega,((omega -exponent (CantorNF a)) . x)) in exp (omega,((omega -exponent (CantorNF (a (+) b))) . x)) by ORDINAL4:24;
then A10: (CantorNF a) . x in exp (omega,((omega -exponent (CantorNF (a (+) b))) . x)) by A7, Th42;
x in dom (omega -leading_coeff (CantorNF (a (+) b))) by A5, Def3;
then (omega -leading_coeff (CantorNF (a (+) b))) . x <> {} by FUNCT_1:def 9;
then 0 c< (omega -leading_coeff (CantorNF (a (+) b))) . x by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in (omega -leading_coeff (CantorNF (a (+) b))) . x by ORDINAL1:11;
then 1 *^ (exp (omega,((omega -exponent (CantorNF (a (+) b))) . x))) c= (CantorNF (a (+) b)) . x by A6, CARD_1:49, ZFMISC_1:31, ORDINAL2:41;
then exp (omega,((omega -exponent (CantorNF (a (+) b))) . x)) c= (CantorNF (a (+) b)) . x by ORDINAL2:39;
hence contradiction by A3, A10; :: thesis: verum
end;
then (omega -leading_coeff (CantorNF (a (+) b))) . x in (omega -leading_coeff (CantorNF a)) . x by A3, A6, A7, ORDINAL3:34;
then A11: omega -leading_coeff ((CantorNF (a (+) b)) . x) in (omega -leading_coeff (CantorNF a)) . x by A5, Def3;
A12: x in dom (omega -exponent (CantorNF a)) by A4, Def1;
then (omega -exponent (CantorNF (a (+) b))) . x in rng (omega -exponent (CantorNF a)) by A8, FUNCT_1:3;
then A13: omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF a)) by A5, Def1;
per cases ( omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF b)) or not omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF b)) ) ;
suppose omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF b)) ; :: thesis: contradiction
then omega -exponent ((CantorNF (a (+) b)) . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by A13, XBOOLE_0:def 4;
then omega -leading_coeff ((CantorNF (a (+) b)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) by A1, A2, A5
.= ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) by A5, A8, Def1
.= ((omega -leading_coeff (CantorNF a)) . x) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) by A12, FUNCT_1:34 ;
then Segm ((omega -leading_coeff (CantorNF a)) . x) c= Segm (omega -leading_coeff ((CantorNF (a (+) b)) . x)) by NAT_1:11, NAT_1:39;
then omega -leading_coeff ((CantorNF (a (+) b)) . x) in omega -leading_coeff ((CantorNF (a (+) b)) . x) by A11;
hence contradiction ; :: thesis: verum
end;
suppose not omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF b)) ; :: thesis: contradiction
then omega -exponent ((CantorNF (a (+) b)) . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by A13, XBOOLE_0:def 5;
then omega -leading_coeff ((CantorNF (a (+) b)) . x) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . x))) by A1, A2, A5
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . x)) by A5, A8, Def1
.= (omega -leading_coeff (CantorNF a)) . x by A12, FUNCT_1:34 ;
hence contradiction by A11; :: thesis: verum
end;
end;