let Y, X be non empty set ; :: thesis: for f being Function of X,Y
for x being Element of X holds Im f,x = {(f . x)}
let f be Function of X,Y; :: thesis: for x being Element of X holds Im f,x = {(f . x)}
let x be Element of X; :: thesis: Im f,x = {(f . x)}
for y being set holds
( y in f .: {x} iff y = f . x )

proof

let y be set ; :: thesis: ( y in f .: {x} iff y = f . x )
thus ( y in f .: {x} implies y = f . x ) :: thesis: ( y = f . x implies y in f .: {x} )

proof

assume y in f .: {x} ; :: thesis: y = f . x
then ex z being set st
( z in dom f & z in {x} & f . z = y ) by FUNCT_1:def 12;
hence y = f . x by TARSKI:def 1; :: thesis: verum

end;

x in {x} by TARSKI:def 1;
hence ( y = f . x implies y in f .: {x} ) by FUNCT_2:43; :: thesis: verum

end;

hence Im f,x = {(f . x)} by TARSKI:def 1; :: thesis: verum