let n be Nat; ( n > 1 implies n |^|^ omega = omega )
assume A1:
n > 1
; n |^|^ omega = omega
deffunc H1( Ordinal) -> Ordinal = n |^|^ $1;
consider phi being Ordinal-Sequence such that
A2:
( dom phi = omega & ( for b being Ordinal st b in omega holds
phi . b = H1(b) ) )
from ORDINAL2:sch 3();
A3:
rng phi c= omega
A5:
n |^|^ omega = lim phi
by A2, Th15;
now ( {} <> omega & ( for b, c being Ordinal st b in omega & omega in c holds
ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) ) ) )thus
{} <> omega
;
for b, c being Ordinal st b in omega & omega in c holds
ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) )let b,
c be
Ordinal;
( b in omega & omega in c implies ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) ) )assume A6:
(
b in omega &
omega in c )
;
ex D being Ordinal st
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) )reconsider x =
b as
Element of
omega by A6;
take D =
n |^|^ x;
( D in dom phi & ( for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c ) ) )thus
D in dom phi
by A2, ORDINAL1:def 12;
for E being Ordinal st D c= E & E in dom phi holds
( b in phi . E & phi . E in c )
x < D
by A1, Th28;
then A7:
b in Segm D
by NAT_1:44;
let E be
Ordinal;
( D c= E & E in dom phi implies ( b in phi . E & phi . E in c ) )assume A8:
(
D c= E &
E in dom phi )
;
( b in phi . E & phi . E in c )then reconsider e =
E as
Element of
omega by A2;
x in Segm e
by A7, A8;
then
(
x < e &
e < n |^|^ e )
by A1, Th28, NAT_1:44;
then A9:
(
x < n |^|^ e &
phi . e = H1(
e) )
by A2, XXREAL_0:2;
phi . E in rng phi
by A8, FUNCT_1:def 3;
then reconsider phiE =
phi . E as
Nat by A3;
b in Segm phiE
by A9, NAT_1:44;
hence
b in phi . E
;
phi . E in c
phi . E in rng phi
by A8, FUNCT_1:def 3;
hence
phi . E in c
by A6, A3, ORDINAL1:10;
verum end;
then
omega is_limes_of phi
by ORDINAL2:def 9;
hence
n |^|^ omega = omega
by A5, ORDINAL2:def 10; verum