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

proof

let z be set ; :: 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 set such that
A1: [z,x] in P * R by Def4;
consider y being set such that
A2: [z,y] in P and
A3: [y,x] in R by A1, Def8;
y in dom R by A3, Def4;
hence z in P " (dom R) by A2, Def14; :: thesis: verum

end;

assume z in P " (dom R) ; :: thesis: z in dom (P * R)
then consider y being set such that
A4: [z,y] in P and
A5: y in dom R by Def14;
consider x being set such that
A6: [y,x] in R by A5, Def4;
[z,x] in P * R by A4, A6, Def8;
hence z in dom (P * R) by Def4; :: thesis: verum

end;

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