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

proof

let x be set ; :: thesis: ( x in (P * R) " Y iff x in P " (R " Y) )
thus ( x in (P * R) " Y implies x in P " (R " Y) ) :: thesis: ( x in P " (R " Y) implies x in (P * R) " Y )

proof

assume x in (P * R) " Y ; :: thesis: x in P " (R " Y)
then consider y being set such that
A1: [x,y] in P * R and
A2: y in Y by Def14;
consider z being set such that
A3: [x,z] in P and
A4: [z,y] in R by A1, Def8;
z in R " Y by A2, A4, Def14;
hence x in P " (R " Y) by A3, Def14; :: thesis: verum

end;

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

end;

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