( rng S c= NAT & rng (R * S) c= rng S ) by Def4, RELAT_1:26;
hence rng (R * S) c= NAT ; :: according to VALUED_0:def 6 :: thesis: verum