let P, R be Relation; :: thesis: rng (P * R) = R .: (rng P)
for z being object holds
( z in rng (P * R) iff z in R .: (rng P) )
proof
let z be object ; :: 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 object such that
A1: [x,z] in P * R by XTUPLE_0:def 13;
consider y being object such that
A2: [x,y] in P and
A3: [y,z] in R by A1, Def6;
y in rng P by A2, XTUPLE_0:def 13;
hence z in R .: (rng P) by A3, Def11; :: thesis: verum
end;
assume z in R .: (rng P) ; :: thesis: z in rng (P * R)
then consider y being object such that
A4: [y,z] in R and
A5: y in rng P by Def11;
consider x being object such that
A6: [x,y] in P by A5, XTUPLE_0:def 13;
[x,z] in P * R by A4, A6, Def6;
hence z in rng (P * R) by XTUPLE_0:def 13; :: thesis: verum
end;
hence rng (P * R) = R .: (rng P) by TARSKI:2; :: thesis: verum