let p be Real; :: thesis: ( 0 < p implies for a, ap being Real_Sequence st a is summable & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = ((Partial_Sums a) . n) to_power p ) holds
( ap is convergent & lim ap = (Sum a) to_power p & ap is non-decreasing & ( for n being Nat holds ap . n <= (Sum a) to_power p ) ) )
assume A1: 0 < p ; :: thesis: for a, ap being Real_Sequence st a is summable & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = ((Partial_Sums a) . n) to_power p ) holds
( ap is convergent & lim ap = (Sum a) to_power p & ap is non-decreasing & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )
let a, ap be Real_Sequence; :: thesis: ( a is summable & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = ((Partial_Sums a) . n) to_power p ) implies ( ap is convergent & lim ap = (Sum a) to_power p & ap is non-decreasing & ( for n being Nat holds ap . n <= (Sum a) to_power p ) ) )
assume that
A2: a is summable and
A3: for n being Nat holds 0 <= a . n and
A4: for n being Nat holds ap . n = ((Partial_Sums a) . n) to_power p ; :: thesis: ( ap is convergent & lim ap = (Sum a) to_power p & ap is non-decreasing & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )
A5: ( Partial_Sums a is convergent & ( for n being Nat holds 0 <= (Partial_Sums a) . n ) ) by A2, A3, Lm2, SERIES_1:def 2;
then lim ap = (lim (Partial_Sums a)) to_power p by A1, A4, Th10;
hence A6: ( ap is convergent & lim ap = (Sum a) to_power p ) by A1, A4, A5, Th10, SERIES_1:def 3; :: thesis: ( ap is non-decreasing & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )
A7: Partial_Sums a is non-decreasing by A3, SERIES_1:16;

now :: thesis: for n, m being Nat st n <= m holds
ap . n <= ap . m

let n, m be Nat; :: thesis: ( n <= m implies ap . n <= ap . m )
assume n <= m ; :: thesis: ap . n <= ap . m
then A8: (Partial_Sums a) . n <= (Partial_Sums a) . m by A7, SEQM_3:6;
A9: ( ap . n = ((Partial_Sums a) . n) to_power p & ap . m = ((Partial_Sums a) . m) to_power p ) by A4;
0 <= (Partial_Sums a) . n by A3, Lm2;
hence ap . n <= ap . m by A1, A9, A8, Th3; :: thesis: verum

end;

hence A10: ap is non-decreasing by SEQM_3:6; :: thesis: for n being Nat holds ap . n <= (Sum a) to_power p
thus for n being Nat holds ap . n <= (Sum a) to_power p by A6, A10, SEQ_4:37; :: thesis: verum