let Y be set ; :: thesis: for x being object
for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
let x be object ; :: thesis: for f being Function holds
( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
let f be Function; :: thesis: ( x in f " Y iff ( [x,(f . x)] in f & f . x in Y ) )
thus ( x in f " Y implies ( [x,(f . x)] in f & f . x in Y ) ) :: thesis: ( [x,(f . x)] in f & f . x in Y implies x in f " Y )

proof

assume x in f " Y ; :: thesis: ( [x,(f . x)] in f & f . x in Y )
then ex y being object st
( [x,y] in f & y in Y ) by RELAT_1:def 14;
hence ( [x,(f . x)] in f & f . x in Y ) by FUNCT_1:1; :: thesis: verum

end;

thus ( [x,(f . x)] in f & f . x in Y implies x in f " Y ) by RELAT_1:def 14; :: thesis: verum