theorem :: FUNCOP_1:84

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