set q = Sgm ((dom p) \ {i});
rng (Sgm ((dom p) \ {i})) = (dom p) \ {i} by FINSEQ_1:def 14;
then rng (Sgm ((dom p) \ {i})) c= dom p by XBOOLE_1:36;
then A2: dom (p * (Sgm ((dom p) \ {i}))) = dom (Sgm ((dom p) \ {i})) by RELAT_1:27;
dom (Sgm ((dom p) \ {i})) = Seg (len (Sgm ((dom p) \ {i}))) by FINSEQ_1:def 3;
hence p * (Sgm ((dom p) \ {i})) is FinSequence by A2, FINSEQ_1:def 2; :: thesis: verum