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:60;
then ( On (dom (psi | (Rank A))) c= On (Rank A) & On (dom (psi | (Rank A))) = dom (psi | (Rank A)) ) by ORDINAL2:9, ORDINAL3:6, RELAT_1:58;
then A1: dom (psi | (Rank A)) c= A by Th12;
A c= Rank A by CLASSES1:38;
then (psi | (Rank A)) | A = psi | A by FUNCT_1:51;
hence psi | (Rank A) = psi | A by A1, RELAT_1:68; :: thesis: verum