( rng S c= COMPLEX & rng (R * S) c= rng S ) by Def1, RELAT_1:26;
hence rng (R * S) c= COMPLEX by XBOOLE_1:1; :: according to VALUED_0:def 1 :: thesis: verum