let R be Relation; :: thesis: for X, Y being set holds (Y |` R) | X = (Y |` R) /\ (R | X)
let X, Y be set ; :: thesis: (Y |` R) | X = (Y |` R) /\ (R | X)

now :: thesis: for z being object holds
( ( z in (Y |` R) | X implies z in (Y |` R) /\ (R | X) ) & ( z in (Y |` R) /\ (R | X) implies z in (Y |` R) | X ) )

let z be object ; :: thesis: ( ( z in (Y |` R) | X implies z in (Y |` R) /\ (R | X) ) & ( z in (Y |` R) /\ (R | X) implies z in (Y |` R) | X ) )

hereby :: thesis: ( z in (Y |` R) /\ (R | X) implies z in (Y |` R) | X )

assume A1: z in (Y |` R) | X ; :: thesis: z in (Y |` R) /\ (R | X)
then consider x, y being object such that
A2: z = [x,y] by RELAT_1:def 1;
A3: ( z in Y |` R & x in X ) by A1, A2, RELAT_1:def 11;
then z in R by A2, RELAT_1:def 12;
then z in R | X by A2, A3, RELAT_1:def 11;
hence z in (Y |` R) /\ (R | X) by A3, XBOOLE_0:def 4; :: thesis: verum

end;

assume z in (Y |` R) /\ (R | X) ; :: thesis: z in (Y |` R) | X
then A4: ( z in Y |` R & z in R | X ) by XBOOLE_0:def 4;
then consider x, y being object such that
A5: z = [x,y] by RELAT_1:def 1;
x in X by A4, A5, RELAT_1:def 11;
hence z in (Y |` R) | X by A4, A5, RELAT_1:def 11; :: thesis: verum

end;

hence (Y |` R) | X = (Y |` R) /\ (R | X) by TARSKI:2; :: thesis: verum