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