theorem :: VALUED_2:50

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)