theorem Th2: :: TOPREALC:2
for c1, c2 being Complex
for f being complex-valued Function holds f (#) (c1 + c2) = (f (#) c1) + (f (#) c2)