theorem :: VALUED_2:51

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)