theorem PPM: :: RVSUM_4:12

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