let a, b be Ordinal; :: thesis: ( ( 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 :: thesis: ( 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)) ; :: thesis: omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0
then 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 ; :: thesis: 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 ; :: thesis: contradiction

hence contradiction by A4, A5, A7, A10, FUNCT_1:def 4; :: thesis: verum

end;

suppose y <> 0 ; :: thesis: contradiction

then 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; :: thesis: verum

end;

end;

end;

hence omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 by A4; :: thesis: verum

end;

assume omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: contradiction

hence contradiction by A14, A15, A17, A20, FUNCT_1:def 4; :: thesis: verum

end;

suppose y <> 0 ; :: thesis: contradiction

then 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; :: thesis: verum

end;

end;

end;

hence omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 by A14; :: thesis: verum