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