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
dom (psi | (Rank A)) c= dom psi by 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, RELAT_1:87;
then A1: dom (psi | (Rank A)) c= A by Th14;
A c= Rank A by CLASSES1:44;
then (psi | (Rank A)) | A = psi | A by FUNCT_1:82;
hence psi | (Rank A) = psi | A by A1, RELAT_1:97; :: thesis: verum