( rng (Del (s,i)) c= rng s & rng s c= A ) by FINSEQ_3:106;
then rng (Del (s,i)) c= A ;
then Del (s,i) is FinSequence of A by FINSEQ_1:def 4;
hence Del (s,i) is Element of A * by FINSEQ_1:def 11; :: thesis: verum