theorem :: RVSUM_4:56

for f being Complex_Sequence
for n being Nat holds XProduct (f | (n + 1)) = (Partial_Product f) . n