theorem ProductA: :: RVSUM_3:25

for f being real-valued positive FinSequence
for i being Nat
for a being Real st i in dom f holds
Product (f +* (i,a)) = ((Product f) * a) / (f . i)