theorem Th5: :: FUNCT_2:5

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 Y