let N be Element of 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

assume A2: r = 0 ; :: thesis: for q being Real st 0 < q holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let q be Real; :: thesis: ( 0 < q implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )
assume A3: 0 < q ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
take k = 0 ; :: thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let m be Element of 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, EUCLID:29;
then |.(((r * seq) . m) - (r * (lim seq))).| = |.((0 * (seq . m)) - (0. (TOP-REAL N))).| by A2, LmDef3
.= |.((0. (TOP-REAL N)) - (0 * (seq . m))).| by Th28
.= |.((0. (TOP-REAL N)) + (- (0 * (seq . m)))).| by EUCLID:41
.= |.(- (0 * (seq . m))).| by EUCLID:27
.= |.(0 * (seq . m)).| by EUCLID:71
.= |.(0. (TOP-REAL N)).| by EUCLID:29
.= 0 by Th24 ;
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

A6: 0 / (abs r) = 0 ;
assume A7: r <> 0 ; :: thesis: for q being Real st 0 < q holds
ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
then A8: 0 < abs r by COMPLEX1:47;
let q be Real; :: thesis: ( 0 < q implies ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q )
assume 0 < q ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
then 0 < q / (abs r) by A8, A6, XREAL_1:74;
then consider n1 being Element of NAT such that
A9: for m being Element of NAT st n1 <= m holds
|.((seq . m) - (lim seq)).| < q / (abs r) by A4, Def10;
take k = n1; :: thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * (lim seq))).| < q
let m be Element of 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 / (abs r) by A9;
A11: 0 <> abs r by A7, COMPLEX1:47;
A12: (abs r) * (q / (abs r)) = (abs r) * (((abs r) ") * q) by XCMPLX_0:def 9
.= ((abs r) * ((abs r) ")) * q
.= 1 * q by A11, XCMPLX_0:def 7
.= q ;
|.(((r * seq) . m) - (r * (lim seq))).| = |.((r * (seq . m)) - (r * (lim seq))).| by LmDef3
.= |.(r * ((seq . m) - (lim seq))).| by EUCLID:49
.= (abs r) * |.((seq . m) - (lim seq)).| by Th8 ;
hence |.(((r * seq) . m) - (r * (lim seq))).| < q by A8, A10, A12, XREAL_1:68; :: thesis: verum

end;

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