theorem Th63: :: MESFUNC5:63

for L, K being ExtREAL_sequence
for c being Real st 0 <= c & ( for n, m being Nat st n <= m holds
L . n <= L . m ) & ( for n being Nat holds K . n = c * (L . n) ) & L is () holds
( ( for n, m being Nat st n <= m holds
K . n <= K . m ) & K is () & K is convergent & lim K = sup (rng K) & lim K = c * (lim L) )