let A be Ordinal; :: thesis: succ A is_cofinal_with 1
deffunc H₁( set ) -> Ordinal = A;
consider psi being Ordinal-Sequence such that
A1: ( dom psi = 1 & ( for B being Ordinal st B in 1 holds
psi . B = H₁(B) ) ) from ORDINAL2:sch 3();
take psi ; :: according to ORDINAL2:def 17 :: thesis: ( dom psi = 1 & rng psi c= succ A & psi is increasing & succ A = sup psi )
thus dom psi = 1 by A1; :: thesis: ( rng psi c= succ A & psi is increasing & succ A = sup psi )
thus rng psi c= succ A :: thesis: ( psi is increasing & succ A = sup psi )

proof

let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in rng psi or e in succ A )
assume e in rng psi ; :: thesis: e in succ A
then consider u being object such that
A2: u in 1 and
A3: e = psi . u by A1, FUNCT_1:def 3;
reconsider u = u as Ordinal by A2;
psi . u = A by A1, A2;
hence e in succ A by A3, ORDINAL1:6; :: thesis: verum

end;

thus psi is increasing by A1, Th14; :: thesis: succ A = sup psi
A4: psi . {} = A by A1, Lm1, ORDINAL1:6;
rng psi = {(psi . {})} by A1, Lm1, FUNCT_1:4;
hence succ A = sup psi by A4, ORDINAL2:23; :: thesis: verum