let P, R be Relation; :: thesis: rng (P * R) c= rng R
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (P * R) or y in rng R )
assume y in rng (P * R) ; :: thesis: y in rng R
then consider x being object such that
A1: [x,y] in P * R by XTUPLE_0:def 13;
ex z being object st
( [x,z] in P & [z,y] in R ) by A1, Def6;
hence y in rng R by XTUPLE_0:def 13; :: thesis: verum