thus rng (Del (fs,a)) c= D1 by FINSEQ_1:def 4; :: according to FINSEQ_1:def 4 :: thesis: verum