let A, B be Ordinal; :: thesis:
given psi being Ordinal-Sequence such that A1: dom psi = succ B and
A2: rng psi c= A and
A3: psi is increasing and
A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis:
reconsider C = psi . B as Ordinal ;
take C ; :: thesis:
thus A c= succ C :: according to XBOOLE_0:def 10 :: thesis:

let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis:
assume a in A ; :: thesis:
then consider b being Ordinal such that
A5: b in rng psi and
A6: a c= b by A4, ORDINAL2:21;
consider e being object such that
A7: e in succ B and
A8: b = psi . e by A1, A5, FUNCT_1:def 3;
reconsider e = e as Ordinal by A7;
e c= B by A7, ORDINAL1:22;
then b c= C by A1, A3, A8, ORDINAL1:6, ORDINAL4:9;
then b in succ C by ORDINAL1:22;
hence a in succ C by A6, ORDINAL1:12; :: thesis:

end;