theorem :: HOLDER_1:11

for p being Real st 0 < p holds
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 ) )