theorem ProdReplace: :: RVSUM_3:27

for f being real-valued positive FinSequence
for i, j being Nat
for a, b being positive Real st i in dom f & j in dom f & i <> j holds
Product (Replace (f,i,j,a,b)) = (((Product f) * a) * b) / ((f . i) * (f . j))