theorem :: PREPOWER:33

for a being Real
for s being Real_Sequence st a > 0 & ( for n being Nat st n >= 1 holds
s . n = n -Root a ) holds
( s is convergent & lim s = 1 )