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

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