theorem Th4: :: FUNCT_2:4

for X, Y being set
for x being object
for f being Function of X,Y st Y <> {} & x in X holds
f . x in rng f