theorem Th4: :: POLYDIFF:4

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