rng (S * R) c= rng R by RELAT_1:26;
hence not 0 in rng (S * R) ; :: according to ORDINAL1:def 15 :: thesis: verum