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