theorem :: FOMODEL0:25

for x being set
for f being Function
for y being non empty set holds
( y = f . x iff x in f " {y} )