let Y be set ; :: thesis: for R being Relation holds R " Y = R " ((rng R) /\ Y)
let R be Relation; :: thesis: R " Y = R " ((rng R) /\ Y)
for x being object holds
( x in R " Y iff x in R " ((rng R) /\ Y) )

proof

let x be object ; :: thesis: ( x in R " Y iff x in R " ((rng R) /\ Y) )
thus ( x in R " Y implies x in R " ((rng R) /\ Y) ) :: thesis: ( x in R " ((rng R) /\ Y) implies x in R " Y )

proof

assume x in R " Y ; :: thesis: x in R " ((rng R) /\ Y)
then consider y being object such that
A1: y in rng R and
A2: [x,y] in R and
A3: y in Y by Th123;
y in (rng R) /\ Y by A1, A3, XBOOLE_0:def 4;
hence x in R " ((rng R) /\ Y) by A2, Def12; :: thesis: verum

end;

assume x in R " ((rng R) /\ Y) ; :: thesis: x in R " Y
then consider y being object such that
y in rng R and
A4: [x,y] in R and
A5: y in (rng R) /\ Y by Th123;
y in Y by A5, XBOOLE_0:def 4;
hence x in R " Y by A4, Def12; :: thesis: verum

end;

hence R " Y = R " ((rng R) /\ Y) by TARSKI:2; :: thesis: verum