theorem Th7: :: POLYDIFF:7

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