theorem Th10: :: HOLDER_1:10

for p being Real st 0 < p holds
for a, ap being Real_Sequence st a is convergent & ( for n being Nat holds 0 <= a . n ) & ( for n being Nat holds ap . n = (a . n) to_power p ) holds
( ap is convergent & lim ap = (lim a) to_power p )