theorem :: RVSUM_4:54

for f being non empty complex-valued XFinSequence holds XProduct (f | 1) = f . 0