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