theorem :: FUNCT_1:3

for x being object
for f being Function st x in dom f holds
f . x in rng f by Def3;