let P, R be Relation; :: thesis: rng (P * R) = R .: (rng P)
for z being set holds
( z in rng (P * R) iff z in R .: (rng P) )

proof

let z be set ; :: thesis: ( z in rng (P * R) iff z in R .: (rng P) )
thus ( z in rng (P * R) implies z in R .: (rng P) ) :: thesis: ( z in R .: (rng P) implies z in rng (P * R) )

proof

assume z in rng (P * R) ; :: thesis: z in R .: (rng P)
then consider x being set such that
A1: [x,z] in P * R by Def5;
consider y being set such that
A2: [x,y] in P and
A3: [y,z] in R by A1, Def8;
y in rng P by A2, Def5;
hence z in R .: (rng P) by A3, Def13; :: thesis: verum

end;

assume z in R .: (rng P) ; :: thesis: z in rng (P * R)
then consider y being set such that
A4: [y,z] in R and
A5: y in rng P by Def13;
consider x being set such that
A6: [x,y] in P by A5, Def5;
[x,z] in P * R by A4, A6, Def8;
hence z in rng (P * R) by Def5; :: thesis: verum

end;

hence rng (P * R) = R .: (rng P) by TARSKI:1; :: thesis: verum