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 = (() . n) to_power p ) holds
( ap is convergent & lim ap = (Sum a) to_power p & ap is V48() & ( 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 = (() . n) to_power p ) holds
( ap is convergent & lim ap = (Sum a) to_power p & ap is V48() & ( 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 = (() . n) to_power p ) implies ( ap is convergent & lim ap = (Sum a) to_power p & ap is V48() & ( 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 = (() . n) to_power p ; :: thesis: ( ap is convergent & lim ap = (Sum a) to_power p & ap is V48() & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )
A5: ( Partial_Sums a is convergent & ( for n being Nat holds 0 <= () . n ) ) by ;
then lim ap = (lim ()) to_power p by A1, A4, Th10;
hence A6: ( ap is convergent & lim ap = (Sum a) to_power p ) by ; :: thesis: ( ap is V48() & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )
A7: Partial_Sums a is V48() by ;
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 <= () . m by ;
A9: ( ap . n = (() . n) to_power p & ap . m = (() . m) to_power p ) by A4;
0 <= () . n by ;
hence ap . n <= ap . m by A1, A9, A8, Th3; :: thesis: verum
end;
hence A10: ap is V48() 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 ; :: thesis: verum