theorem :: FINSEQ_9:35

for a being positive Real
for f being nonnegative-yielding FinSequence of REAL st ( for k being Element of NAT st k in dom f holds
f . k <= a ) holds
Product f <= a |^ (len f)