theorem Th6: :: VALUED_1:6
for f being complex-valued Function
for r being Complex
for c being object holds (r (#) f) . c = r * (f . c)