let P, R be Relation; :: thesis: ( dom P c= rng R implies rng (R * P) = rng P )
assume A1: for y being object st y in dom P holds
y in rng R ; :: according to TARSKI:def 3 :: thesis: rng (R * P) = rng P
thus rng (R * P) c= rng P by Th20; :: according to XBOOLE_0:def 10 :: thesis: rng P c= rng (R * P)
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng P or z in rng (R * P) )
assume z in rng P ; :: thesis: z in rng (R * P)
then consider y being object such that
A2: [y,z] in P by XTUPLE_0:def 13;
y in dom P by A2, XTUPLE_0:def 12;
then y in rng R by A1;
then consider x being object such that
A3: [x,y] in R by XTUPLE_0:def 13;
[x,z] in R * P by A2, A3, Def6;
hence z in rng (R * P) by XTUPLE_0:def 13; :: thesis: verum