let x, Y be set ; :: thesis: for R being Relation holds
( x in R " Y iff ex y being set 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 set st
( y in rng R & [x,y] in R & y in Y ) )
thus ( x in R " Y implies ex y being set st
( y in rng R & [x,y] in R & y in Y ) ) :: thesis: ( ex y being set 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 set st
( y in rng R & [x,y] in R & y in Y )
then consider y being set such that
A1: ( [x,y] in R & y in Y ) by Def14;
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, Def5; :: thesis: verum

end;

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