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