let N be Nat; :: thesis: for r being Real
for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)
let r be Real; :: thesis: for seq being Real_Sequence of N st seq is convergent holds
lim (r * seq) = r * (lim seq)
let seq be Real_Sequence of N; :: thesis: ( seq is convergent implies lim (r * seq) = r * (lim seq) )

A1: now :: thesis: ( r = 0 implies for q being Real st 0 < q holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )

assume A2: r = 0 ; :: thesis: for q being Real st 0 < q holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let q be Real; :: thesis: ( 0 < q implies ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )
assume A3: 0 < q ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
reconsider k = 0 as Nat ;
take k = k; :: thesis: for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let m be Nat; :: thesis: ( k <= m implies |.(((r * seq) . m) - (r * (lim seq))).| < q )
assume k <= m ; :: thesis: |.(((r * seq) . m) - (r * (lim seq))).| < q
r * (lim seq) = 0. (TOP-REAL N) by A2, RLVECT_1:10;
then |.(((r * seq) . m) - (r * (lim seq))).| = |.((0 * (seq . m)) - (0. (TOP-REAL N))).| by A2, Th5
.= |.((0. (TOP-REAL N)) - (0 * (seq . m))).| by Th27
.= |.((0. (TOP-REAL N)) + (- (0 * (seq . m)))).|
.= |.(- (0 * (seq . m))).| by RLVECT_1:4
.= |.(0 * (seq . m)).| by EUCLID:71
.= |.(0. (TOP-REAL N)).| by RLVECT_1:10
.= 0 by Th23 ;
hence |.(((r * seq) . m) - (r * (lim seq))).| < q by A3; :: thesis: verum

end;

assume A4: seq is convergent ; :: thesis: lim (r * seq) = r * (lim seq)

A5: now :: thesis: ( r <> 0 implies for q being Real st 0 < q holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )

A6: 0 / |.r.| = 0 ;
assume A7: r <> 0 ; :: thesis: for q being Real st 0 < q holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
then A8: 0 < |.r.| by COMPLEX1:47;
let q be Real; :: thesis: ( 0 < q implies ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )
assume 0 < q ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
then 0 < q / |.r.| by A8, A6, XREAL_1:74;
then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < q / |.r.| by A4, Def9;
take k = n1; :: thesis: for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let m be Nat; :: thesis: ( k <= m implies |.(((r * seq) . m) - (r * (lim seq))).| < q )
assume k <= m ; :: thesis: |.(((r * seq) . m) - (r * (lim seq))).| < q
then A10: |.((seq . m) - (lim seq)).| < q / |.r.| by A9;
A11: 0 <> |.r.| by A7, COMPLEX1:47;
A12: |.r.| * (q / |.r.|) = |.r.| * ((|.r.| ") * q) by XCMPLX_0:def 9
.= (|.r.| * (|.r.| ")) * q
.= 1 * q by A11, XCMPLX_0:def 7
.= q ;
|.(((r * seq) . m) - (r * (lim seq))).| = |.((r * (seq . m)) - (r * (lim seq))).| by Th5
.= |.(r * ((seq . m) - (lim seq))).| by RLVECT_1:34
.= |.r.| * |.((seq . m) - (lim seq)).| by Th7 ;
hence |.(((r * seq) . m) - (r * (lim seq))).| < q by A8, A10, A12, XREAL_1:68; :: thesis: verum

end;

r * seq is convergent by A4, Th38;
hence lim (r * seq) = r * (lim seq) by A1, A5, Def9; :: thesis: verum