let a, b be Ordinal; :: thesis: omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)

per cases ( a (+) b <> {} or a (+) b = {} ) ;

suppose A1: a (+) b <> {} ; :: thesis: omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)

( omega -exponent a c= omega -exponent (a (+) b) & omega -exponent b c= omega -exponent (a (+) b) ) by Th22, Th99;
then A2: (omega -exponent a) \/ (omega -exponent b) c= omega -exponent (a (+) b) by XBOOLE_1:8;
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set C0 = CantorNF (a (+) b);
0 c< dom (CantorNF (a (+) b)) by A1, XBOOLE_1:2, XBOOLE_0:def 8;
then A3: 0 in dom (CantorNF (a (+) b)) by ORDINAL1:11;
then 0 in dom (omega -exponent (CantorNF (a (+) b))) by Def1;
then (omega -exponent (CantorNF (a (+) b))) . 0 in rng (omega -exponent (CantorNF (a (+) b))) by FUNCT_1:3;
then (omega -exponent (CantorNF (a (+) b))) . 0 in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by Th76;

per cases then ( (omega -exponent (CantorNF (a (+) b))) . 0 in rng (omega -exponent (CantorNF a)) or (omega -exponent (CantorNF (a (+) b))) . 0 in rng (omega -exponent (CantorNF b)) ) by XBOOLE_0:def 3;

suppose A4: (omega -exponent (CantorNF (a (+) b))) . 0 in rng (omega -exponent (CantorNF a)) ; :: thesis: omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)

then omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF a)) by A3, Def1;
then A5: omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF a)) . 0 by Th95;
omega -exponent (CantorNF a) <> {} by A4;
then 0 c< dom (omega -exponent (CantorNF a)) by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in dom (omega -exponent (CantorNF a)) by ORDINAL1:11;
then A6: 0 in dom (CantorNF a) by Def1;
omega -exponent (a (+) b) = omega -exponent (Sum^ (CantorNF (a (+) b)))
.= omega -exponent ((CantorNF (a (+) b)) . 0) by Th44
.= omega -exponent ((CantorNF a) . 0) by A5, A6, Def1
.= omega -exponent (Sum^ (CantorNF a)) by Th44
.= omega -exponent a ;
then omega -exponent (a (+) b) c= (omega -exponent a) \/ (omega -exponent b) by XBOOLE_1:7;
hence omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b) by A2, XBOOLE_0:def 10; :: thesis: verum

end;

suppose A7: (omega -exponent (CantorNF (a (+) b))) . 0 in rng (omega -exponent (CantorNF b)) ; :: thesis: omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)

then omega -exponent ((CantorNF (a (+) b)) . 0) in rng (omega -exponent (CantorNF b)) by A3, Def1;
then A8: omega -exponent ((CantorNF (a (+) b)) . 0) = (omega -exponent (CantorNF b)) . 0 by Th95;
omega -exponent (CantorNF b) <> {} by A7;
then 0 c< dom (omega -exponent (CantorNF b)) by XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in dom (omega -exponent (CantorNF b)) by ORDINAL1:11;
then A9: 0 in dom (CantorNF b) by Def1;
omega -exponent (a (+) b) = omega -exponent (Sum^ (CantorNF (a (+) b)))
.= omega -exponent ((CantorNF (a (+) b)) . 0) by Th44
.= omega -exponent ((CantorNF b) . 0) by A8, A9, Def1
.= omega -exponent (Sum^ (CantorNF b)) by Th44
.= omega -exponent b ;
then omega -exponent (a (+) b) c= (omega -exponent a) \/ (omega -exponent b) by XBOOLE_1:7;
hence omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b) by A2, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

suppose a (+) b = {} ; :: thesis: omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b)

then ( a = 0 & b = 0 ) ;
hence omega -exponent (a (+) b) = (omega -exponent a) \/ (omega -exponent b) ; :: thesis: verum

end;

end;