let i, j be Nat; :: thesis: for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) & i <= j holds
Sum (s ^\ j) <= Sum (s ^\ i)
let s be Real_Sequence; :: thesis: ( s is summable & ( for n being Nat holds 0 <= s . n ) & i <= j implies Sum (s ^\ j) <= Sum (s ^\ i) )
assume A1: ( s is summable & ( for n being Nat holds 0 <= s . n ) ) ; :: thesis: ( not i <= j or Sum (s ^\ j) <= Sum (s ^\ i) )
assume i <= j ; :: thesis: Sum (s ^\ j) <= Sum (s ^\ i)

per cases then ( i = j or i < j ) by XXREAL_0:1;

suppose i = j ; :: thesis: Sum (s ^\ j) <= Sum (s ^\ i)

hence Sum (s ^\ j) <= Sum (s ^\ i) ; :: thesis: verum

end;

suppose i < j ; :: thesis: Sum (s ^\ j) <= Sum (s ^\ i)

then i + 1 <= j by NAT_1:13;
then 0 <= j - (i + 1) by XREAL_1:48;
then reconsider k = j - (i + 1) as Nat ;
s ^\ i is summable by A1, SERIES_1:12;
then A2: Sum (s ^\ i) = ((Partial_Sums (s ^\ i)) . k) + (Sum ((s ^\ i) ^\ (k + 1))) by SERIES_1:15
.= ((Partial_Sums (s ^\ i)) . k) + (Sum (s ^\ (i + (k + 1)))) by NAT_1:48
.= ((Partial_Sums (s ^\ i)) . k) + (Sum (s ^\ j)) ;
for n being Nat holds 0 <= (s ^\ i) . n

proof

let n be Nat; :: thesis: 0 <= (s ^\ i) . n
0 <= s . (i + n) by A1;
hence 0 <= (s ^\ i) . n by NAT_1:def 3; :: thesis: verum

end;

hence Sum (s ^\ j) <= Sum (s ^\ i) by A2, PartialNonneg, XREAL_1:31; :: thesis: verum

end;

end;