theorem :: RVSUM_1:110

for F being FinSequence of COMPLEX holds Product F = multcomplex $$ F ;