theorem Th90: :: PREPOWER:90

for a being Real
for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)