let n be Nat; :: thesis:
assume A1: n > 1 ; :: thesis:
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:
assume x in rng phi ; :: thesis:
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:

end;

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

now :: thesis:

thus {} <> omega ; :: thesis:
let b, c be Ordinal; :: thesis:
assume A6: ( b in omega & omega in c ) ; :: thesis:
reconsider x = b as Element of omega by A6;
take D = n |^|^ x; :: thesis:
thus D in dom phi by A2, ORDINAL1:def 12; :: thesis:
x < D by A1, Th28;
then A7: b in Segm D by NAT_1:44;
let E be Ordinal; :: thesis:
assume A8: ( D c= E & E in dom phi ) ; :: thesis:
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 rng phi by A8, FUNCT_1:def 3;
hence phi . E in c by A6, A3, ORDINAL1:10; :: thesis:

end;

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