( rng S c= ExtREAL & rng (R * S) c= rng S ) by Def2, RELAT_1:26;
hence rng (R * S) c= ExtREAL ; :: according to VALUED_0:def 2 :: thesis: verum