rng (R * S) c= rng S by Th45;
hence not {} in rng (R * S) by Def9; :: according to RELAT_1:def 9 :: thesis: verum