let P, R be Relation; :: thesis: rng (P * R) c= rng R
let y be set ; :: 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 set such that
A1: [x,y] in P * R by Def5;
ex z being set st
( [x,z] in P & [z,y] in R ) by A1, Def8;
hence y in rng R by Def5; :: thesis: verum