let f1, f2 be nonnegative-yielding FinSequence of REAL ; :: thesis: ( len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
f1 . k >= f2 . k ) implies Product f1 >= Product f2 )
assume A1: ( len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
f1 . k >= f2 . k ) ) ; :: thesis: Product f1 >= Product f2
per cases ( ex l being Element of NAT st
( l in dom f2 & f2 . l = 0 ) or for l being Element of NAT st l in dom f2 holds
f2 . l <> 0 ) ;
suppose ex l being Element of NAT st
( l in dom f2 & f2 . l = 0 ) ; :: thesis: Product f1 >= Product f2
hence Product f1 >= Product f2 by RVSUM_1:103; :: thesis: verum
end;
suppose for l being Element of NAT st l in dom f2 holds
f2 . l <> 0 ; :: thesis: Product f1 >= Product f2
then for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k > 0 ) by A1, XXREAL_0:1;
hence Product f1 >= Product f2 by A1, NAT_4:54; :: thesis: verum
end;
end;