theorem Th13: :: VALUED_2:13

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