let Y be set ; :: thesis: for x being object
for R being Relation holds
( x in R " Y iff ex y being object st
( y in rng R & [x,y] in R & y in Y ) )
let x be object ; :: thesis: for R being Relation holds
( x in R " Y iff ex y being object st
( y in rng R & [x,y] in R & y in Y ) )
let R be Relation; :: thesis: ( x in R " Y iff ex y being object st
( y in rng R & [x,y] in R & y in Y ) )
thus ( x in R " Y implies ex y being object st
( y in rng R & [x,y] in R & y in Y ) ) :: thesis: ( ex y being object st
( y in rng R & [x,y] in R & y in Y ) implies x in R " Y )

proof

assume x in R " Y ; :: thesis: ex y being object st
( y in rng R & [x,y] in R & y in Y )
then consider y being object such that
A1: ( [x,y] in R & y in Y ) by Def12;
take y ; :: thesis: ( y in rng R & [x,y] in R & y in Y )
thus ( y in rng R & [x,y] in R & y in Y ) by A1, XTUPLE_0:def 13; :: thesis: verum

end;

thus ( ex y being object st
( y in rng R & [x,y] in R & y in Y ) implies x in R " Y ) by Def12; :: thesis: verum