theorem PAP: :: RVSUM_4:9

for f being complex-valued FinSequence
for n being Nat holds Product f = (Product (f | n)) * (Product (f /^ n))