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