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 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 = ((Partial_Sums a) . 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 = ((Partial_Sums a) . 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 = ((Partial_Sums a) . 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 <= (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 V48() & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )

A7: Partial_Sums a is V48() by A3, SERIES_1:16;

thus for n being Nat holds ap . n <= (Sum a) to_power p by A6, A10, SEQ_4:37; :: thesis: verum

( 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 = ((Partial_Sums a) . 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 = ((Partial_Sums a) . 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 = ((Partial_Sums a) . 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 <= (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 V48() & ( for n being Nat holds ap . n <= (Sum a) to_power p ) )

A7: Partial_Sums a is V48() by A3, SERIES_1:16;

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

ap . n <= ap . m

hence A10:
ap is V48()
by SEQM_3:6; :: thesis: for n being Nat holds ap . n <= (Sum a) to_power pap . 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;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

thus for n being Nat holds ap . n <= (Sum a) to_power p by A6, A10, SEQ_4:37; :: thesis: verum