let n be Nat; :: thesis: ( n > 1 implies n |^|^ omega = omega )
assume Z0: n > 1 ; :: thesis: n |^|^ omega = omega
deffunc H₁( Ordinal) -> Ordinal = n |^|^ $1;
consider phi being Ordinal-Sequence such that
A1: ( dom phi = omega & ( for b being ordinal number st b in omega holds
phi . b = H₁(b) ) ) from ORDINAL2:sch 3();
AA: rng phi c= omega

proof

let x be set ; :: 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 set such that
B1: ( a in dom phi & x = phi . a ) by FUNCT_1:def 5;
reconsider a = a as Element of omega by A1, B1;
x = n |^|^ a by A1, B1;
hence x in omega by ORDINAL1:def 13; :: thesis: verum

end;

A2: n |^|^ omega = lim phi by A1, Th2;

now

thus {} <> omega ; :: thesis: for b, c being ordinal number 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 number ; :: 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 A3: ( 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 A3;
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 A1, ORDINAL1:def 13; :: 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 Z0, ThA1;
then A4: b in D by NAT_1:45;
let E be Ordinal; :: thesis: ( D c= E & E in dom phi implies ( b in phi . E & phi . E in c ) )
assume A5: ( 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 A1;
( x < e & e < n |^|^ e ) by Z0, ThA1, NAT_1:45, A4, A5;
then A6: ( x < n |^|^ e & phi . e = H₁(e) ) by A1, XXREAL_0:2;
phi . E in rng phi by A5, FUNCT_1:def 5;
hence ( b in phi . E & phi . E in c ) by A3, A6, ORDINAL1:19, NAT_1:45, AA; :: thesis: verum

end;

then omega is_limes_of phi by ORDINAL2:def 13;
hence n |^|^ omega = omega by A2, ORDINAL2:def 14; :: thesis: verum