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