let X, Y 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 object holds
( y in f .: {x} iff y = f . x )

proof

let y be object ; :: 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 object st
( z in dom f & z in {x} & f . z = y ) by FUNCT_1:def 6;
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:35; :: thesis: verum

end;

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