let N be Element of NAT ; :: thesis: for r being Real
for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent
let r be Real; :: thesis: for seq being Real_Sequence of N st seq is convergent holds
r * seq is convergent
let seq be Real_Sequence of N; :: thesis: ( seq is convergent implies r * seq is convergent )
assume seq is convergent ; :: thesis: r * seq is convergent
then consider g1 being Point of (TOP-REAL N) such that
A1: for q being Real st 0 < q holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - g1).| < q by Def9;
set g = r * g1;

A2: now

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

end;

now

assume A10: 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 * g1)).| < 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 * g1)).| < q )
assume A11: 0 < q ; :: thesis: ex k being Element of NAT st
for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
take k = 0 ; :: thesis: for m being Element of NAT st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
let m be Element of NAT ; :: thesis: ( k <= m implies |.(((r * seq) . m) - (r * g1)).| < q )
assume k <= m ; :: thesis: |.(((r * seq) . m) - (r * g1)).| < q
|.(((r * seq) . m) - (r * g1)).| = |.(((0 * seq) . m) - (0. (TOP-REAL N))).| by A10, EUCLID:29
.= |.((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 * (seq . m)).| by LmDef3
.= |.(0. (TOP-REAL N)).| by EUCLID:29
.= 0 by Th24 ;
hence |.(((r * seq) . m) - (r * g1)).| < q by A11; :: thesis: verum

end;

hence r * seq is convergent by A2, Def9; :: thesis: verum