theorem :: VALUED_2:48

for x being object
for X being set
for Y being complex-functions-membered set
for c being Complex
for f being PartFunc of X,Y st x in dom (f [-] c) holds
(f [-] c) . x = (f . x) - c by Def37;