let a1, a2, b be Ordinal; :: thesis: ( a1 in exp (omega,b) & a2 in exp (omega,b) implies a1 +^ a2 in exp (omega,b) )
assume A1: ( a1 in exp (omega,b) & a2 in exp (omega,b) ) ; :: thesis: a1 +^ a2 in exp (omega,b)

per cases ( ( 0 in a1 & 0 in a2 ) or not 0 in a1 or not 0 in a2 ) ;

suppose A2: ( 0 in a1 & 0 in a2 ) ; :: thesis: a1 +^ a2 in exp (omega,b)

set d1 = omega -exponent a1;
set d2 = omega -exponent a2;
consider n1 being Nat, c1 being Ordinal such that
A3: ( a1 = (n1 *^ (exp (omega,(omega -exponent a1)))) +^ c1 & 0 in Segm n1 & c1 in exp (omega,(omega -exponent a1)) ) by A2, ORDINAL5:62;
consider n2 being Nat, c2 being Ordinal such that
A4: ( a2 = (n2 *^ (exp (omega,(omega -exponent a2)))) +^ c2 & 0 in Segm n2 & c2 in exp (omega,(omega -exponent a2)) ) by A2, ORDINAL5:62;
A5: omega -exponent a1 in b

proof

assume not omega -exponent a1 in b ; :: thesis: contradiction
then A6: exp (omega,b) c= exp (omega,(omega -exponent a1)) by ORDINAL1:16, ORDINAL4:27;
1 c= n1 by ORDINAL1:21, Lm1, A3;
then 1 *^ (exp (omega,b)) c= n1 *^ (exp (omega,(omega -exponent a1))) by A6, ORDINAL3:20;
then A7: exp (omega,b) c= n1 *^ (exp (omega,(omega -exponent a1))) by ORDINAL2:39;
0 c= c1 ;
then (exp (omega,b)) +^ 0 c= a1 by A3, A7, ORDINAL3:18;
then exp (omega,b) c= a1 by ORDINAL2:27;
hence contradiction by A1, ORDINAL1:5; :: thesis: verum

end;

A8: omega -exponent a2 in b

proof

assume not omega -exponent a2 in b ; :: thesis: contradiction
then A9: exp (omega,b) c= exp (omega,(omega -exponent a2)) by ORDINAL1:16, ORDINAL4:27;
1 c= n2 by ORDINAL1:21, Lm1, A4;
then 1 *^ (exp (omega,b)) c= n2 *^ (exp (omega,(omega -exponent a2))) by A9, ORDINAL3:20;
then A10: exp (omega,b) c= n2 *^ (exp (omega,(omega -exponent a2))) by ORDINAL2:39;
0 c= c2 ;
then (exp (omega,b)) +^ 0 c= a2 by A4, A10, ORDINAL3:18;
then exp (omega,b) c= a2 by ORDINAL2:27;
hence contradiction by A1, ORDINAL1:5; :: thesis: verum

end;

a1 in (n1 *^ (exp (omega,(omega -exponent a1)))) +^ (exp (omega,(omega -exponent a1))) by A3, ORDINAL2:32;
then A11: a1 in (succ n1) *^ (exp (omega,(omega -exponent a1))) by ORDINAL2:36;
a2 in (n2 *^ (exp (omega,(omega -exponent a2)))) +^ (exp (omega,(omega -exponent a2))) by A4, ORDINAL2:32;
then A12: a2 in (succ n2) *^ (exp (omega,(omega -exponent a2))) by ORDINAL2:36;

per cases ( omega -exponent a1 c= omega -exponent a2 or omega -exponent a2 in omega -exponent a1 ) by ORDINAL1:16;

suppose omega -exponent a1 c= omega -exponent a2 ; :: thesis: a1 +^ a2 in exp (omega,b)

then exp (omega,(omega -exponent a1)) c= exp (omega,(omega -exponent a2)) by ORDINAL4:27;
then (succ n1) *^ (exp (omega,(omega -exponent a1))) c= (succ n1) *^ (exp (omega,(omega -exponent a2))) by ORDINAL2:42;
then a1 +^ a2 in ((succ n1) *^ (exp (omega,(omega -exponent a2)))) +^ ((succ n2) *^ (exp (omega,(omega -exponent a2)))) by A11, A12, ORDINAL3:17;
then A13: a1 +^ a2 in ((succ n1) +^ (succ n2)) *^ (exp (omega,(omega -exponent a2))) by ORDINAL3:46;
((succ n1) +^ (succ n2)) *^ (exp (omega,(omega -exponent a2))) in exp (omega,b) by A8, ORDINAL5:7;
hence a1 +^ a2 in exp (omega,b) by A13, ORDINAL1:10; :: thesis: verum

end;

suppose omega -exponent a2 in omega -exponent a1 ; :: thesis: a1 +^ a2 in exp (omega,b)

then exp (omega,(omega -exponent a2)) c= exp (omega,(omega -exponent a1)) by ORDINAL1:def 2, ORDINAL4:27;
then (succ n2) *^ (exp (omega,(omega -exponent a2))) c= (succ n2) *^ (exp (omega,(omega -exponent a1))) by ORDINAL2:42;
then a1 +^ a2 in ((succ n1) *^ (exp (omega,(omega -exponent a1)))) +^ ((succ n2) *^ (exp (omega,(omega -exponent a1)))) by A11, A12, ORDINAL3:17;
then A14: a1 +^ a2 in ((succ n1) +^ (succ n2)) *^ (exp (omega,(omega -exponent a1))) by ORDINAL3:46;
((succ n1) +^ (succ n2)) *^ (exp (omega,(omega -exponent a1))) in exp (omega,b) by A5, ORDINAL5:7;
hence a1 +^ a2 in exp (omega,b) by A14, ORDINAL1:10; :: thesis: verum

end;

end;

end;

suppose not 0 in a1 ; :: thesis: a1 +^ a2 in exp (omega,b)

then a1 = 0 by ORDINAL1:16, XBOOLE_1:3;
hence a1 +^ a2 in exp (omega,b) by A1, ORDINAL2:30; :: thesis: verum

end;

suppose not 0 in a2 ; :: thesis: a1 +^ a2 in exp (omega,b)

then a2 = 0 by ORDINAL1:16, XBOOLE_1:3;
hence a1 +^ a2 in exp (omega,b) by A1, ORDINAL2:27; :: thesis: verum

end;

end;