let x be set ; :: thesis: for f being Function
for y being non empty set holds
( y = f . x iff x in f " {y} )
let f be Function; :: thesis: for y being non empty set holds
( y = f . x iff x in f " {y} )
let y be non empty set ; :: thesis: ( y = f . x iff x in f " {y} )
thus ( y = f . x implies x in f " {y} ) :: thesis: ( x in f " {y} implies y = f . x )

proof

assume y = f . x ; :: thesis: x in f " {y}
then ( x in dom f & f . x in {y} ) by FUNCT_1:def 2, TARSKI:def 1;
hence x in f " {y} by FUNCT_1:def 7; :: thesis: verum

end;

assume x in f " {y} ; :: thesis: y = f . x
then ( x in dom f & f . x in {y} ) by FUNCT_1:def 7;
hence y = f . x by TARSKI:def 1; :: thesis: verum