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: ( proj1 psi = 1 & proj2 psi c= succ A & psi is increasing & succ A = sup psi )
thus dom psi = 1 by A1; :: thesis: ( proj2 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 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 :: thesis: succ A = sup psi

proof

let B be Ordinal; :: according to ORDINAL2:def 12 :: thesis: for b₁ being set holds
( not B in b₁ or not b₁ in proj1 psi or psi . B in psi . b₁ )
let C be Ordinal; :: thesis: ( not B in C or not C in proj1 psi or psi . B in psi . C )
assume that
A4: B in C and
A5: C in dom psi ; :: thesis: psi . B in psi . C
thus psi . B in psi . C by A1, A4, A5, Th17; :: thesis: verum

end;

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