let a be Ordinal; :: thesis: ( 1 in a implies a |^|^ omega is limit_ordinal )
assume A1: 1 in a ; :: thesis: a |^|^ omega is limit_ordinal
deffunc H1( Ordinal) -> Ordinal = a |^|^ $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();
 phi is increasing
proof
let b be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b1 being set holds
( not b in b1 or not b1 in dom phi or phi . b in phi . b1 )
let c be Ordinal; :: thesis: ( not b in c or not c in dom phi or phi . b in phi . c )
assume A3: ( b in c & c in dom phi ) ; :: thesis: phi . b in phi . c
then reconsider b = b, c = c as Element of NAT by A2, ORDINAL1:10;
b in Segm c by A3;
then b < c by NAT_1:44;
then ( phi . b = H1(b) & H1(b) in H1(c) ) by A1, A2, Th24;
hence phi . b in phi . c by A2; :: thesis: verum
end;
then ( lim phi = sup phi & sup phi is limit_ordinal ) by A2, ORDINAL4:8, ORDINAL4:16;
hence a |^|^ omega is limit_ordinal by A2, Th15; :: thesis: verum