theorem Th1: :: POLYDIFF:1

for f being complex-valued Function holds 0 + f = f