let F be FinSequence of REAL ; :: thesis: ( ( for i being Element of dom F holds F . i > 0 ) implies Product F > 0 )
assume for i being Element of dom F holds F . i > 0 ; :: thesis: Product F > 0
then for j being Element of NAT st j in dom F holds
F . j > 0 ;
hence Product F > 0 by NAT_4:42; :: thesis: verum