let a, b be Ordinal; ( ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 ) & ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 ) )
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set C0 = CantorNF (a (+) b);
A2:
rng (omega -exponent (CantorNF (a (+) b))) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))
by Th76;
hereby ( omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) implies omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 )
assume
omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a))
;
omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0then consider x being
object such that A4:
(
x in dom (omega -exponent (CantorNF a)) &
(omega -exponent (CantorNF a)) . x = omega -exponent ((CantorNF (a (+) b)) . 0) )
by FUNCT_1:def 3;
reconsider x =
x as
Ordinal by A4;
x = 0
proof
assume A5:
x <> 0
;
contradiction
then
0 c< x
by XBOOLE_1:2, XBOOLE_0:def 8;
then A6:
0 in x
by ORDINAL1:11;
then A7:
0 in dom (omega -exponent (CantorNF a))
by A4, ORDINAL1:10;
then
(omega -exponent (CantorNF a)) . 0 in rng (omega -exponent (CantorNF a))
by FUNCT_1:3;
then
(omega -exponent (CantorNF a)) . 0 in rng (omega -exponent (CantorNF (a (+) b)))
by A2, XBOOLE_1:7, TARSKI:def 3;
then consider y being
object such that A8:
(
y in dom (omega -exponent (CantorNF (a (+) b))) &
(omega -exponent (CantorNF (a (+) b))) . y = (omega -exponent (CantorNF a)) . 0 )
by FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A8;
A9:
y in dom (CantorNF (a (+) b))
by A8, Def1;
then A10:
omega -exponent ((CantorNF (a (+) b)) . y) = (omega -exponent (CantorNF a)) . 0
by A8, Def1;
per cases
( y = 0 or y <> 0 )
;
suppose
y <> 0
;
contradictionthen
0 c< y
by XBOOLE_1:2, XBOOLE_0:def 8;
then
0 in y
by ORDINAL1:11;
then A11:
(omega -exponent (CantorNF a)) . 0 in (omega -exponent (CantorNF a)) . x
by A4, A9, A10, ORDINAL5:def 11;
A12:
x in dom (CantorNF a)
by A4, Def1;
then
omega -exponent ((CantorNF a) . 0) in (omega -exponent (CantorNF a)) . x
by A11, Def1, A6, ORDINAL1:10;
then
omega -exponent ((CantorNF a) . 0) in omega -exponent ((CantorNF a) . x)
by A12, Def1;
hence
contradiction
by A6, A12, ORDINAL5:def 11;
verum end;
end; hence
omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0
by A4;
verum
end;
assume
omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b))
; omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0
then consider x being object such that
A14:
( x in dom (omega -exponent (CantorNF b)) & (omega -exponent (CantorNF b)) . x = omega -exponent ((CantorNF (a (+) b)) . 0) )
by FUNCT_1:def 3;
reconsider x = x as Ordinal by A14;
x = 0
proof
assume A15:
x <> 0
;
contradiction
then
0 c< x
by XBOOLE_1:2, XBOOLE_0:def 8;
then A16:
0 in x
by ORDINAL1:11;
then A17:
0 in dom (omega -exponent (CantorNF b))
by A14, ORDINAL1:10;
then
(omega -exponent (CantorNF b)) . 0 in rng (omega -exponent (CantorNF b))
by FUNCT_1:3;
then
(omega -exponent (CantorNF b)) . 0 in rng (omega -exponent (CantorNF (a (+) b)))
by A2, XBOOLE_1:7, TARSKI:def 3;
then consider y being
object such that A18:
(
y in dom (omega -exponent (CantorNF (a (+) b))) &
(omega -exponent (CantorNF (a (+) b))) . y = (omega -exponent (CantorNF b)) . 0 )
by FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A18;
A19:
y in dom (CantorNF (a (+) b))
by A18, Def1;
then A20:
omega -exponent ((CantorNF (a (+) b)) . y) = (omega -exponent (CantorNF b)) . 0
by A18, Def1;
per cases
( y = 0 or y <> 0 )
;
suppose
y <> 0
;
contradictionthen
0 c< y
by XBOOLE_1:2, XBOOLE_0:def 8;
then
0 in y
by ORDINAL1:11;
then A21:
(omega -exponent (CantorNF b)) . 0 in (omega -exponent (CantorNF b)) . x
by A14, A19, A20, ORDINAL5:def 11;
A22:
x in dom (CantorNF b)
by A14, Def1;
then
omega -exponent ((CantorNF b) . 0) in (omega -exponent (CantorNF b)) . x
by A21, Def1, A16, ORDINAL1:10;
then
omega -exponent ((CantorNF b) . 0) in omega -exponent ((CantorNF b) . x)
by A22, Def1;
hence
contradiction
by A16, A22, ORDINAL5:def 11;
verum end;
end;
hence
omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0
by A14; verum