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

now

let n, m be Element of NAT ; :: thesis: ( n <= m implies ap . n <= ap . m )
assume A9: n <= m ; :: thesis: ap . n <= ap . m
A10: ap . n = ((Partial_Sums a) . n) to_power p by A4;
A11: ap . m = ((Partial_Sums a) . m) to_power p by A4;
A12: (Partial_Sums a) . n <= (Partial_Sums a) . m by A8, A9, SEQM_3:12;
0 <= (Partial_Sums a) . n by A3, Lm2;
hence ap . n <= ap . m by A1, A10, A11, A12, Th3; :: thesis: verum

end;

hence A13: ap is non-decreasing by SEQM_3:12; :: thesis: for n being Element of NAT holds ap . n <= (Sum a) to_power p
ap is bounded by A6, SEQ_2:27;
then ap is bounded_above ;
hence for n being Element of NAT holds ap . n <= (Sum a) to_power p by A7, A13, SEQ_4:54; :: thesis: verum