reconsider g = f as real-valued FinSequence ;

per cases ( g is positive-yielding or not g is positive-yielding ) ;

suppose g is positive-yielding ; :: thesis: not Product f is negative

then for x being Real st x in rng g holds
x > 0 by PARTFUN3:def 1;
then for k being Element of NAT st k in dom g holds
g . k > 0 by FUNCT_1:3;
hence not Product f is negative by NAT_4:42; :: thesis: verum

end;

suppose B1: not g is positive-yielding ; :: thesis: not Product f is negative

ex i being object st
( i in dom g & g . i = 0 )

proof

consider r being Real such that
C1: ( r in rng g & r <= 0 ) by B1, PARTFUN3:def 1;
r = 0 by PARTFUN3:def 4, C1;
hence ex i being object st
( i in dom g & g . i = 0 ) by C1, FUNCT_1:def 3; :: thesis: verum

end;

hence not Product f is negative by RVSUM_1:103; :: thesis: verum

end;

end;