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