let r be Real; :: thesis: for seq being Real_Sequence st seq is convergent holds
lim (r (#) seq) = r * (lim seq)
let seq be Real_Sequence; :: thesis: ( seq is convergent implies lim (r (#) seq) = r * (lim seq) )
assume A1: seq is convergent ; :: thesis: lim (r (#) seq) = r * (lim seq)

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

assume A3: r = 0 ; :: thesis: for p being Real st 0 < p holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p
let p be Real; :: thesis: ( 0 < p implies ex k being Nat st
for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p )
assume A4: 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p
reconsider k = 0 as Nat ;
take k = k; :: thesis: for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p
let m be Nat; :: thesis: ( k <= m implies |.(((r (#) seq) . m) - (r * (lim seq))).| < p )
assume k <= m ; :: thesis: |.(((r (#) seq) . m) - (r * (lim seq))).| < p
|.(((r (#) seq) . m) - (r * (lim seq))).| = |.((0 * (seq . m)) - 0).| by A3, SEQ_1:9
.= 0 by ABSVALUE:2 ;
hence |.(((r (#) seq) . m) - (r * (lim seq))).| < p by A4; :: thesis: verum

end;

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

assume A5: r <> 0 ; :: thesis: for p being Real st 0 < p holds
ex k being Nat st
for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p
then A6: 0 < |.r.| by COMPLEX1:47;
let p be Real; :: thesis: ( 0 < p implies ex k being Nat st
for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p )
assume A7: 0 < p ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p
A8: 0 <> |.r.| by A5, COMPLEX1:47;
0 < p / |.r.| by A6, A7;
then consider n1 being Nat such that
A9: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p / |.r.| by A1, Def6;
take k = n1; :: thesis: for m being Nat st k <= m holds
|.(((r (#) seq) . m) - (r * (lim seq))).| < p
let m be Nat; :: thesis: ( k <= m implies |.(((r (#) seq) . m) - (r * (lim seq))).| < p )
assume k <= m ; :: thesis: |.(((r (#) seq) . m) - (r * (lim seq))).| < p
then A10: |.((seq . m) - (lim seq)).| < p / |.r.| by A9;
A11: |.(((r (#) seq) . m) - (r * (lim seq))).| = |.((r * (seq . m)) - (r * (lim seq))).| by SEQ_1:9
.= |.(r * ((seq . m) - (lim seq))).|
.= |.r.| * |.((seq . m) - (lim seq)).| by COMPLEX1:65 ;
|.r.| * (p / |.r.|) = |.r.| * ((|.r.| ") * p) by XCMPLX_0:def 9
.= (|.r.| * (|.r.| ")) * p
.= 1 * p by A8, XCMPLX_0:def 7
.= p ;
hence |.(((r (#) seq) . m) - (r * (lim seq))).| < p by A6, A10, A11, XREAL_1:68; :: thesis: verum

end;

hence lim (r (#) seq) = r * (lim seq) by A1, A2, Def6; :: thesis: verum