let f be Function; :: thesis: for x, y being set st x in f " {y} holds
f . x = y
let x, y be set ; :: thesis: ( x in f " {y} implies f . x = y )
assume A1: x in f " {y} ; :: thesis: f . x = y
f . x in {y} by A1, FUNCT_1:def 7;
hence f . x = y by TARSKI:def 1; :: thesis: verum