let rF be real-valued XFinSequence; :: thesis: for r being Real st ( for n being Nat st n in dom rF holds
rF . n <= r ) holds
Sum rF <= (len rF) * r
let r be Real; :: thesis: ( ( for n being Nat st n in dom rF holds
rF . n <= r ) implies Sum rF <= (len rF) * r )
set L = (len rF) --> r;
assume A1: for n being Nat st n in dom rF holds
rF . n <= r ; :: thesis: Sum rF <= (len rF) * r
A2: len ((len rF) --> r) = len rF by FUNCOP_1:13;

now :: thesis: for n being Nat st n in dom rF holds
rF . n <= ((len rF) --> r) . n

let n be Nat; :: thesis: ( n in dom rF implies rF . n <= ((len rF) --> r) . n )
assume n in dom rF ; :: thesis: rF . n <= ((len rF) --> r) . n
then ( rF . n <= r & ((len rF) --> r) . n = r ) by A1, FUNCOP_1:7;
hence rF . n <= ((len rF) --> r) . n ; :: thesis: verum

end;

then Sum rF <= Sum ((len rF) --> r) by Th56, A2;
hence Sum rF <= (len rF) * r by Th57; :: thesis: verum