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 = (R_EAL c) * (L . n) ) & L is without-infty holds
( ( for n, m being Nat st n <= m holds
K . n <= K . m ) & K is without-infty & K is convergent & lim K = sup (rng K) & lim K = (R_EAL 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 = (R_EAL c) * (L . n) ) & L is without-infty implies ( ( for n, m being Nat st n <= m holds
K . n <= K . m ) & K is without-infty & K is convergent & lim K = sup (rng K) & lim K = (R_EAL 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 = (R_EAL c) * (L . n) and
A4: L is without-infty ; :: thesis: ( ( for n, m being Nat st n <= m holds
K . n <= K . m ) & K is without-infty & K is convergent & lim K = sup (rng K) & lim K = (R_EAL c) * (lim L) )

hereby :: thesis: ( K is without-infty & K is convergent & lim K = sup (rng K) & lim K = (R_EAL 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 (R_EAL c) * (L . n) <= (R_EAL c) * (L . m) by A1, A2, XXREAL_3:82;
then K . n <= (R_EAL c) * (L . m) by A3;
hence K . n <= K . m by A3; :: thesis: verum

end;

thus K is without-infty by A1, A3, A4, Th68; :: thesis: ( K is convergent & lim K = sup (rng K) & lim K = (R_EAL c) * (lim L) )
thus ( K is convergent & lim K = sup (rng K) ) by A5, Th60; :: thesis: lim K = (R_EAL c) * (lim L)
( sup (rng K) = lim K & sup (rng L) = lim L ) by A2, A5, Th60;
hence lim K = (R_EAL c) * (lim L) by A1, A3, A4, Th68; :: thesis: verum