theorem :: FUNCOP_1:17

for h being Function
for A being set
for x being object st x in dom h holds
h * (A --> x) = A --> (h . x)