theorem :: FUNCT_1:50

for X being set
for x being object
for f being Function st x in dom f & x in X holds
f . x in rng (f | X)