theorem Th4: :: SETWISEO:7

for X, Y being non empty set
for f being Function of X,Y
for x being Element of X holds x in f " {(f . x)}