theorem Th5: :: POLYDIFF:5

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