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