theorem Th8: :: TOPREAL6:9

for rr being Real
for i, j being Nat st rr <> 0 & j <= i holds
Product ((i -' j) |-> rr) = (Product (i |-> rr)) / (Product (j |-> rr))