let X be set ; :: thesis: for P, R being Relation holds (P * R) .: X = R .: (P .: X)
let P, R be Relation; :: thesis: (P * R) .: X = R .: (P .: X)
for y being object holds
( y in (P * R) .: X iff y in R .: (P .: X) )

proof

let y be object ; :: thesis: ( y in (P * R) .: X iff y in R .: (P .: X) )
thus ( y in (P * R) .: X implies y in R .: (P .: X) ) :: thesis: ( y in R .: (P .: X) implies y in (P * R) .: X )

proof

assume y in (P * R) .: X ; :: thesis: y in R .: (P .: X)
then consider x being object such that
A1: [x,y] in P * R and
A2: x in X by Def11;
consider z being object such that
A3: [x,z] in P and
A4: [z,y] in R by A1, Def6;
z in P .: X by A2, A3, Def11;
hence y in R .: (P .: X) by A4, Def11; :: thesis: verum

end;

assume y in R .: (P .: X) ; :: thesis: y in (P * R) .: X
then consider x being object such that
A5: [x,y] in R and
A6: x in P .: X by Def11;
consider z being object such that
A7: [z,x] in P and
A8: z in X by A6, Def11;
[z,y] in P * R by A5, A7, Def6;
hence y in (P * R) .: X by A8, Def11; :: thesis: verum

end;

hence (P * R) .: X = R .: (P .: X) by TARSKI:2; :: thesis: verum