let a, b, c be Ordinal; :: thesis: ( a in exp (omega,c) & b in exp (omega,c) implies a (+) b in exp (omega,c) )
assume A1: ( a in exp (omega,c) & b in exp (omega,c) ) ; :: thesis: a (+) b in exp (omega,c)
per cases ( a = 0 or b = 0 or ( a <> {} & b <> {} ) ) ;
suppose a = 0 ; :: thesis: a (+) b in exp (omega,c)
hence a (+) b in exp (omega,c) by A1, Th82; :: thesis: verum
end;
suppose b = 0 ; :: thesis: a (+) b in exp (omega,c)
hence a (+) b in exp (omega,c) by A1, Th82; :: thesis: verum
end;
suppose A2: ( a <> {} & b <> {} ) ; :: thesis: a (+) b in exp (omega,c)
then ( 0 c< a & 0 c< b ) by XBOOLE_1:2, XBOOLE_0:def 8;
then ( 0 in a & 0 in b ) by ORDINAL1:11;
then ( omega -exponent a in c & omega -exponent b in c ) by A1, Th23;
then (omega -exponent a) \/ (omega -exponent b) in c by ORDINAL3:12;
then A3: omega -exponent (a (+) b) in c by Th100;
A4: not c c= omega -exponent (a (+) b) 0 c< a (+) b by A2, XBOOLE_1:2, XBOOLE_0:def 8;
then 0 in a (+) b by ORDINAL1:11;
then not exp (omega,c) c= a (+) b by A4, ORDINAL5:def 10;
hence a (+) b in exp (omega,c) by ORDINAL1:16; :: thesis: verum
end;
end;