theorem Th41: :: NAT_4:42

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