theorem Th7: :: TOPREAL6:8

for rr being Real
for j being Nat holds
( ( j <> 0 & rr = 0 ) iff Product (j |-> rr) = 0 )