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:159 ;
then S .:^ (R .: X) = ((R * (S ` )) .: X) `
.= ((R * (S ` )) ` ) .:^ X by Th50 ;
hence S .:^ (R .: X) = ((R * (S ` )) ` ) .:^ X ; :: thesis: verum