( rng S c= REAL & rng (R * S) c= rng S ) by Def3, RELAT_1:45;
hence rng (R * S) c= REAL by XBOOLE_1:1; :: according to VALUED_0:def 3 :: thesis: verum