( rng fs c= D & rng (Del (fs,a)) c= rng fs ) by FINSEQ_3:106, RELAT_1:def 19;
hence rng (Del (fs,a)) c= D ; :: according to FINSEQ_1:def 4 :: thesis: verum