theorem :: FUNCT_4:7

for x being object
for f being Function st x in dom f holds
x .--> (f . x) c= f