let i be Nat; :: thesis: for s being Real_Sequence st s is summable & ( for n being Nat holds 0 <= s . n ) holds
Sum (s ^\ i) <= Sum s
let s be Real_Sequence; :: thesis: ( s is summable & ( for n being Nat holds 0 <= s . n ) implies Sum (s ^\ i) <= Sum s )
assume ( s is summable & ( for n being Nat holds 0 <= s . n ) ) ; :: thesis: Sum (s ^\ i) <= Sum s
then Sum (s ^\ i) <= Sum (s ^\ 0) by SumMono;
hence Sum (s ^\ i) <= Sum s by NAT_1:47; :: thesis: verum