theorem PSPROD: :: LOPBAN11:7

for F being FinSequence of REAL st ( for i being Element of dom F holds F . i > 0 ) holds
Product F > 0