let x be object ; :: thesis: for f being Function st x in dom f holds
Im (f,x) = {(f . x)}
let f be Function; :: thesis: ( x in dom f implies Im (f,x) = {(f . x)} )
assume A1: x in dom f ; :: thesis: Im (f,x) = {(f . x)}
for y being object holds
( y in f .: {x} iff y in {(f . x)} )

proof

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

proof

assume y in f .: {x} ; :: thesis: y in {(f . x)}
then consider z being object such that
z in dom f and
A2: z in {x} and
A3: y = f . z by Def6;
z = x by A2, TARSKI:def 1;
hence y in {(f . x)} by A3, TARSKI:def 1; :: thesis: verum

end;

assume y in {(f . x)} ; :: thesis: y in f .: {x}
then A4: y = f . x by TARSKI:def 1;
x in {x} by TARSKI:def 1;
hence y in f .: {x} by A1, A4, Def6; :: thesis: verum

end;

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