let a be Real; :: thesis:
let f be FinSequence of REAL ; :: thesis:
assume A0: for k being Element of NAT st k in dom f holds
( 0 < f . k & f . k <= a ) ; :: thesis:
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 )

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

end;