let a1, a2, b be Ordinal; ( 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) )
; 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 )
;
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
;
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;
verum
end; A8:
omega -exponent a2 in b
proof
assume
not
omega -exponent a2 in b
;
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;
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
;
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;
verum end; suppose
omega -exponent a2 in omega -exponent a1
;
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;
verum end; end;