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;