theorem Th52: :: NAT_4:53

for f being FinSequence of NAT
for p being Prime st Product f <> 0 holds
p |-count (Product f) = Sum (p |-count f)