theorem Th6: :: TOPREAL6:7

for rr being Real
for n being Nat holds Product ((n + 1) |-> rr) = (Product (n |-> rr)) * rr