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