let a be positive Real; :: thesis: 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)
let f be nonnegative-yielding FinSequence of REAL ; :: thesis: ( ( for k being Element of NAT st k in dom f holds
f . k <= a ) implies Product f <= a |^ (len f) )
assume A1: for k being Element of NAT st k in dom f holds
f . k <= a ; :: thesis: Product f <= a |^ (len f)
a in REAL by XREAL_0:def 1;
then reconsider g = (len f) |-> a as FinSequence of REAL by FINSEQ_2:63;
reconsider g = g as positive-yielding FinSequence of REAL ;
A2: len f = len g ;
for k being Element of NAT st k in dom f holds
g . k >= f . k

proof

let k be Element of NAT ; :: thesis: ( k in dom f implies g . k >= f . k )
assume B1: k in dom f ; :: thesis: g . k >= f . k
g . k = a by B1, Lmkdf;
hence g . k >= f . k by A1, B1; :: thesis: verum

end;

then Product f <= Product g by A2, N454;
hence Product f <= a |^ (len f) by NEWTON:def 1; :: thesis: verum