set q = Sgm ((dom p) \ {i});
A1: (Seg (len p)) \ {i} c= Seg (len p) by XBOOLE_1:36;
dom p = Seg (len p) by FINSEQ_1:def 3;
then rng (Sgm ((dom p) \ {i})) c= dom p by A1, FINSEQ_1:def 13;
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