theorem Th16: :: VALUED_2:16

for c1, c2 being Complex
for g being complex-valued Function holds (g (#) c1) (#) c2 = g (#) (c1 * c2)