let n be Nat; :: thesis: ( n > 1 implies n |^|^ omega = omega )
assume A1: n > 1 ; :: thesis: n |^|^ omega = omega
deffunc H₁( 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 = H₁(b) ) ) from ORDINAL2:sch 3();
A3: rng phi c= omega

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng phi or x in omega )
assume x in rng phi ; :: thesis: x in omega
then consider a being object such that
A4: ( a in dom phi & x = phi . a ) by FUNCT_1:def 3;
reconsider a = a as Element of omega by A2, A4;
x = n |^|^ a by A2, A4;
hence x in omega by ORDINAL1:def 12; :: thesis: verum

end;

A5: n |^|^ omega = lim phi by A2, Th15;

now :: thesis: ( {} <> 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 ; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( 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; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: ( 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 = H₁(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 ; :: thesis: 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; :: thesis: verum

end;

then omega is_limes_of phi by ORDINAL2:def 9;
hence n |^|^ omega = omega by A5, ORDINAL2:def 10; :: thesis: verum