theorem :: FINSEQ_9:31

for a being Real
for f being FinSequence of REAL st ( for k being Element of NAT st k in dom f holds
( 0 < f . k & f . k <= a ) ) holds
Product f <= Product ((len f) |-> a)