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;

given y being set such that y in rng R and
A2: ( [x,y] in R & y in Y ) ; :: thesis: x in R " Y
thus x in R " Y by A2, Def14; :: thesis: verum