let a, b be Ordinal; ( 0 in a & omega c= b implies a |^|^ b = a |^|^ omega )
assume A1:
0 in a
; ( not omega c= b or a |^|^ b = a |^|^ omega )
assume
omega c= b
; a |^|^ b = a |^|^ omega
then A2:
b = omega +^ (b -^ omega)
by ORDINAL3:def 5;
defpred S1[ Ordinal] means a |^|^ (omega +^ $1) = a |^|^ omega;
A3:
S1[ 0 ]
by ORDINAL2:27;
A4:
for c being Ordinal st S1[c] holds
S1[ succ c]
A6:
for c being Ordinal st c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) holds
S1[c]
proof
let c be
Ordinal;
( c <> 0 & c is limit_ordinal & ( for b being Ordinal st b in c holds
S1[b] ) implies S1[c] )
assume A7:
(
c <> 0 &
c is
limit_ordinal )
;
( ex b being Ordinal st
( b in c & not S1[b] ) or S1[c] )
assume A8:
for
b being
Ordinal st
b in c holds
S1[
b]
;
S1[c]
deffunc H1(
Ordinal)
-> Ordinal =
a |^|^ $1;
consider f being
Ordinal-Sequence such that A9:
(
dom f = omega +^ c & ( for
b being
Ordinal st
b in omega +^ c holds
f . b = H1(
b) ) )
from ORDINAL2:sch 3();
(
omega +^ c <> {} &
omega +^ c is
limit_ordinal )
by A7, ORDINAL3:26, ORDINAL3:29;
then A10:
a |^|^ (omega +^ c) = lim f
by A9, Th15;
now ( a |^|^ omega <> {} & ( for B, C being Ordinal st B in a |^|^ omega & a |^|^ omega in C holds
ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) ) ) )
a c= a |^|^ omega
by A1, Th23;
hence
a |^|^ omega <> {}
by A1;
for B, C being Ordinal st B in a |^|^ omega & a |^|^ omega in C holds
ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )let B,
C be
Ordinal;
( B in a |^|^ omega & a |^|^ omega in C implies ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) ) )assume A11:
(
B in a |^|^ omega &
a |^|^ omega in C )
;
ex D being set st
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )take D =
omega ;
( D in dom f & ( for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C ) ) )
(
omega +^ {} = omega &
{} in c )
by A7, ORDINAL2:27, ORDINAL3:8;
hence
D in dom f
by A9, ORDINAL2:32;
for E being Ordinal st D c= E & E in dom f holds
( B in f . E & f . E in C )let E be
Ordinal;
( D c= E & E in dom f implies ( B in f . E & f . E in C ) )assume A12:
(
D c= E &
E in dom f )
;
( B in f . E & f . E in C )then
E -^ D in (omega +^ c) -^ omega
by A9, ORDINAL3:53;
then
E -^ D in c
by ORDINAL3:52;
then
S1[
E -^ D]
by A8;
then
a |^|^ omega = a |^|^ E
by A12, ORDINAL3:def 5;
hence
(
B in f . E &
f . E in C )
by A9, A11, A12;
verum end;
then
a |^|^ omega is_limes_of f
by ORDINAL2:def 9;
hence
S1[
c]
by A10, ORDINAL2:def 10;
verum
end;
for c being Ordinal holds S1[c]
from ORDINAL2:sch 1(A3, A4, A6);
hence
a |^|^ b = a |^|^ omega
by A2; verum