theorem PPN: :: RVSUM_4:11

for f being Complex_Sequence
for n being Nat st f . n = 0 holds
(Partial_Product f) . n = 0