for f1, f2 being FinSequence of REAL st len f1 = len f2 & ( for k being Element of NAT st k in dom f2 holds
( f1 . k >= f2 . k & f2 . k >= 0 ) ) holds
Product f1 >= Product f2