let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for x being Element of X holds x in f " {(f . x)}
let f be Function of X,Y; :: thesis: for x being Element of X holds x in f " {(f . x)}
let x be Element of X; :: thesis: x in f " {(f . x)}
f . x in {(f . x)} by TARSKI:def 1;
hence x in f " {(f . x)} by FUNCT_2:38; :: thesis: verum