theorem COMSEQ324: :: RVSUM_4:13

for n being Nat holds (Partial_Product (seq_const 0c)) . n = 0