theorem Th11: :: FUNCT_2:11

for X, Y being set
for y being object
for f being Function of X,Y st y in rng f holds
ex x being object st
( x in X & f . x = y )