rng (M | A) c= rng M by RELAT_1:99;
hence not {} in rng (M | A) by RELAT_1:def 9; :: according to RELAT_1:def 9 :: thesis: verum