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

proof

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

end;

hence Product f <= Product ((len f) |-> a) by A1, NAT_4:54; :: thesis: verum