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 21 :: 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 set ; :: 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 set such that
A2: ( u in 1 & e = psi . u ) by A1, FUNCT_1:def 5;
reconsider u = u as Ordinal by A2;
psi . u = A by A1, A2;
hence e in succ A by A2, ORDINAL1:10; :: thesis: verum

end;

thus psi is increasing :: thesis: succ A = sup psi

proof

let B be Ordinal; :: according to ORDINAL2:def 16 :: thesis: for b₁ being set holds
( not B in b₁ or not b₁ in dom psi or psi . B in psi . b₁ )
let C be Ordinal; :: thesis: ( not B in C or not C in dom psi or psi . B in psi . C )
assume ( B in C & C in dom psi ) ; :: thesis: psi . B in psi . C
hence psi . B in psi . C by A1, Th17; :: thesis: verum

end;

( dom psi = {{} } & {} in 1 ) by A1, Lm1, ORDINAL1:10;
then ( rng psi = {(psi . {} )} & psi . {} = A & sup psi = sup (rng psi) ) by A1, FUNCT_1:14;
hence succ A = sup psi by ORDINAL2:31; :: thesis: verum