let P, R be Relation; :: thesis: dom (P * R) = P " (dom R)
for z being object holds
( z in dom (P * R) iff z in P " (dom R) )

proof

let z be object ; :: thesis: ( z in dom (P * R) iff z in P " (dom R) )
thus ( z in dom (P * R) implies z in P " (dom R) ) :: thesis: ( z in P " (dom R) implies z in dom (P * R) )

proof

assume z in dom (P * R) ; :: thesis: z in P " (dom R)
then consider x being object such that
A1: [z,x] in P * R by XTUPLE_0:def 12;
consider y being object such that
A2: [z,y] in P and
A3: [y,x] in R by A1, Def6;
y in dom R by A3, XTUPLE_0:def 12;
hence z in P " (dom R) by A2, Def12; :: thesis: verum

end;

assume z in P " (dom R) ; :: thesis: z in dom (P * R)
then consider y being object such that
A4: [z,y] in P and
A5: y in dom R by Def12;
consider x being object such that
A6: [y,x] in R by A5, XTUPLE_0:def 12;
[z,x] in P * R by A4, A6, Def6;
hence z in dom (P * R) by XTUPLE_0:def 12; :: thesis: verum

end;

hence dom (P * R) = P " (dom R) by TARSKI:2; :: thesis: verum