reconsider F = f as FinSequence of REAL by RVSUM_1:145;
for k being Element of NAT st k in dom F holds
F . k > 0 by PosDef;
hence Product f is positive by NAT_4:42; :: thesis: verum