theorem :: VALUED_2:52

for X being set
for Y being complex-functions-membered set
for c1, c2 being Complex
for f being PartFunc of X,Y holds (f [-] c1) [-] c2 = f [-] (c1 + c2)