let A, B, C be set ; :: thesis: for X being Subset of A
for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
let X be Subset of A; :: thesis: for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
let R be Relation of A,B; :: thesis: for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
let S be Relation of B,C; :: thesis: S .:^ (R .: X) = ((R * (S `)) `) .:^ X
(S .:^ (R .: X)) ` = (S `) .: (R .: X) by Th49
.= (R * (S `)) .: X by RELAT_1:126 ;
then S .:^ (R .: X) = ((R * (S `)) .: X) `
.= ((R * (S `)) `) .:^ X by Th50 ;
hence S .:^ (R .: X) = ((R * (S `)) `) .:^ X ; :: thesis: verum