( rng S c= RAT & rng (R * S) c= rng S ) by Def3r, RELAT_1:26;
hence rng (R * S) c= RAT ; :: according to VALUED_0:def 4 :: thesis: verum