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;

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

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) )

thus
K is ()
by A1, A3, A4, Th62; :: thesis: ( 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;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

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