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)

proof

assume c c= omega -exponent (a (+) b) ; :: thesis: contradiction
then omega -exponent (a (+) b) in omega -exponent (a (+) b) by A3;
hence contradiction ; :: thesis: verum

end;

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;