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 object ; :: 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 not a in R .:^ X by XBOOLE_0:def 5;
then consider x being set such that
A2: x in X and
A3: not a in Im (R,x) by A1, Th25;
A4: not [x,a] in R by A3, Th9;
[x,a] in [:A,B:] by A1, A2, ZFMISC_1:87;
then [x,a] in [:A,B:] \ R by A4, XBOOLE_0:def 5;
hence a in (R `) .: X by A2, RELAT_1:def 13; :: thesis: verum

end;

let a be object ; :: 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 object such that
A5: [x,a] in R ` and
A6: x in X by RELAT_1:def 13;
A7: not [x,a] in R by A5, XBOOLE_0:def 5;
assume not a in (R .:^ X) ` ; :: thesis: contradiction
then A8: ( 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 A9: 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 A9, Th24;
hence [x,a] in R by Th9; :: thesis: verum

end;

hence contradiction by A5, A6, A7, A8, ZFMISC_1:87; :: thesis: verum