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