thus rng (f1 ^ f2) c= D1 by FINSEQ_1:def 4; :: according to FINSEQ_1:def 4 :: thesis: verum