theorem Th3: :: POLYDIFF:3

for c being Complex
for f being complex-valued Function holds c + f = ((dom f) --> c) + f