theorem :: NEWTON04:16

for f, g being FinSequence of COMPLEX
for i being object holds (f (#) g) . i = (f . i) * (g . i)