theorem :: LOPBAN11:3

for F being FinSequence of REAL st ( for k being Element of NAT st k in dom F holds
0 <= F . k ) holds
0 <= Product F