let a, b be Ordinal; :: thesis: for x being object holds (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x
let x be object ; :: thesis: (omega -exponent (CantorNF a)) . x c= (omega -exponent (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);
assume not (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x ; :: thesis: contradiction
then A1: (omega -exponent (CantorNF (a (+) b))) . x in (omega -exponent (CantorNF a)) . x by ORDINAL1:16;
then x in dom (omega -exponent (CantorNF a)) by FUNCT_1:def 2;
then reconsider x = x as Ordinal ;
defpred S₁[ Ordinal] means (omega -exponent (CantorNF (a (+) b))) . $1 in (omega -exponent (CantorNF a)) . $1;
A2: ex z being Ordinal st S₁[z]

proof

take x ; :: thesis: S₁[x]
thus S₁[x] by A1; :: thesis: verum

end;

consider y being Ordinal such that
A3: ( S₁[y] & ( for z being Ordinal st S₁[z] holds
y c= z ) ) from ORDINAL1:sch 1(A2);
A4: rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by Th76;
A5: y in dom (omega -exponent (CantorNF a)) by A3, FUNCT_1:def 2;
then (omega -exponent (CantorNF a)) . y in rng (omega -exponent (CantorNF a)) by FUNCT_1:3;
then (omega -exponent (CantorNF a)) . y in rng (omega -exponent (CantorNF (a (+) b))) by A4, XBOOLE_1:7, TARSKI:def 3;
then consider z being object such that
A6: ( z in dom (omega -exponent (CantorNF (a (+) b))) & (omega -exponent (CantorNF (a (+) b))) . z = (omega -exponent (CantorNF a)) . y ) by FUNCT_1:def 3;
reconsider z = z as Ordinal by A6;
A7: z in dom (CantorNF (a (+) b)) by A6, Def1;
A8: z in y

proof

assume not z in y ; :: thesis: contradiction

per cases then ( z = y or y in z ) by ORDINAL1:14;

suppose z = y ; :: thesis: contradiction

hence contradiction by A3, A6; :: thesis: verum

end;

suppose A9: y in z ; :: thesis: contradiction

then omega -exponent ((CantorNF (a (+) b)) . z) in omega -exponent ((CantorNF (a (+) b)) . y) by A7, ORDINAL5:def 11;
then (omega -exponent (CantorNF a)) . y in omega -exponent ((CantorNF (a (+) b)) . y) by A6, A7, Def1;
hence contradiction by A3, A7, A9, Def1, ORDINAL1:10; :: thesis: verum

end;

end;

end;

A10: y in dom (CantorNF a) by A5, Def1;
then omega -exponent ((CantorNF a) . y) in omega -exponent ((CantorNF a) . z) by A8, ORDINAL5:def 11;
then (omega -exponent (CantorNF a)) . y in omega -exponent ((CantorNF a) . z) by A10, Def1;
then (omega -exponent (CantorNF a)) . y in (omega -exponent (CantorNF a)) . z by A8, A10, Def1, ORDINAL1:10;
then y c= z by A3, A6;
then z in z by A8;
hence contradiction ; :: thesis: verum