( rng R c= A & rng (S * R) c= rng R ) by Def19, Th45;
hence rng (S * R) c= A by XBOOLE_1:1; :: according to RELAT_1:def 19 :: thesis: verum