let L, K be ExtREAL_sequence; :: thesis: 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) )
let c be Real; :: thesis: ( 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 () implies ( ( 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) ) )
assume that
A1: 0 <= c and
A2: for n, m being Nat st n <= m holds
L . n <= L . m and
A3: for n being Nat holds K . n = c * (L . n) and
A4: L is () ; :: thesis: ( ( 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) )
A5: sup (rng L) = lim L by A2, Th54;
hereby :: thesis: ( K is () & K is convergent & lim K = sup (rng K) & lim K = c * (lim L) )
let n, m be Nat; :: thesis: ( n <= m implies K . n <= K . m )
assume n <= m ; :: thesis: K . n <= K . m
then c * (L . n) <= c * (L . m) by A1, A2, XXREAL_3:71;
then K . n <= c * (L . m) by A3;
hence K . n <= K . m by A3; :: thesis: verum
end;
thus K is () by A1, A3, A4, Th62; :: thesis: ( K is convergent & lim K = sup (rng K) & lim K = c * (lim L) )
thus ( K is convergent & lim K = sup (rng K) ) by A6, Th54; :: thesis: lim K = c * (lim L)
sup (rng K) = lim K by A6, Th54;
hence lim K = c * (lim L) by A1, A3, A4, A5, Th62; :: thesis: verum