theorem :: NEWTON04:16

for f, g being complex-valued Function
for i being object holds (f (#) g) . i = (f . i) * (g . i) by VALUED_1:5;