let a, b be Ordinal; for x being object holds (omega -exponent (CantorNF a)) . x c= (omega -exponent (CantorNF (a (+) b))) . x
let x be object ; (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
; 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 S1[ Ordinal] means (omega -exponent (CantorNF (a (+) b))) . $1 in (omega -exponent (CantorNF a)) . $1;
A2:
ex z being Ordinal st S1[z]
proof
take
x
;
S1[x]
thus
S1[
x]
by A1;
verum
end;
consider y being Ordinal such that
A3:
( S1[y] & ( for z being Ordinal st S1[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
;
contradiction
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
; verum