theorem Th14: :: VALUED_2:14

for c1, c2 being Complex
for g being complex-valued Function holds (g - c1) + c2 = g - (c1 - c2)