consider k being Nat such that
A2: dom p c= Seg k by Def12;
dom (X |` p) c= dom p by FUNCT_1:56;
hence X |` p is FinSubsequence-like by A2, XBOOLE_1:1; :: thesis: verum