theorem Th12: :: VALUED_2:12

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