let A, B be set ; :: thesis: for X being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X) ` = (R ` ) .: X
let X be Subset of A; :: thesis: for R being Subset of [:A,B:] holds (R .:^ X) ` = (R ` ) .: X
let R be Subset of [:A,B:]; :: thesis: (R .:^ X) ` = (R ` ) .: X
thus (R .:^ X) ` c= (R ` ) .: X :: according to XBOOLE_0:def 10 :: thesis: (R ` ) .: X c= (R .:^ X) `

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (R .:^ X) ` or a in (R ` ) .: X )
assume A1: a in (R .:^ X) ` ; :: thesis: a in (R ` ) .: X
then ( a in B & not a in R .:^ X ) by XBOOLE_0:def 5;
then consider x being set such that
A2: ( x in X & not a in Im R,x ) by Th25;
A3: not [x,a] in R by A2, Th9;
[x,a] in [:A,B:] by A1, A2, ZFMISC_1:106;
then [x,a] in [:A,B:] \ R by A3, XBOOLE_0:def 5;
hence a in (R ` ) .: X by A2, RELAT_1:def 13; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (R ` ) .: X or a in (R .:^ X) ` )
assume a in (R ` ) .: X ; :: thesis: a in (R .:^ X) `
then consider x being set such that
A4: ( [x,a] in R ` & x in X ) by RELAT_1:def 13;
A5: ( [x,a] in [:A,B:] & not [x,a] in R ) by A4, XBOOLE_0:def 5;
assume not a in (R .:^ X) ` ; :: thesis: contradiction
then A6: ( not a in B or a in R .:^ X ) by XBOOLE_0:def 5;
( a in R .:^ X implies for x being set st x in X holds
[x,a] in R )

proof

assume A7: a in R .:^ X ; :: thesis: for x being set st x in X holds
[x,a] in R
let x be set ; :: thesis: ( x in X implies [x,a] in R )
assume x in X ; :: thesis: [x,a] in R
then a in Im R,x by A7, Th24;
hence [x,a] in R by Th9; :: thesis: verum

end;

hence contradiction by A4, A5, A6, ZFMISC_1:106; :: thesis: verum