let A be Ordinal; :: thesis: for psi being Ordinal-Sequence holds psi | (Rank A) = psi | A
let psi be Ordinal-Sequence; :: thesis: psi | (Rank A) = psi | A
A c= Rank A by CLASSES1:44;
then A1: ( (psi | (Rank A)) | A = psi | A & dom (psi | (Rank A)) c= Rank A & dom (psi | (Rank A)) c= dom psi ) by FUNCT_1:82, RELAT_1:87, RELAT_1:89;
then ( On (dom (psi | (Rank A))) c= On (Rank A) & On (dom (psi | (Rank A))) = dom (psi | (Rank A)) ) by ORDINAL2:11, ORDINAL3:8;
then dom (psi | (Rank A)) c= A by Th14;
hence psi | (Rank A) = psi | A by A1, RELAT_1:97; :: thesis: verum