let N be 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 Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < q ;
set g = r * g1;
A2: 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 * g1)).| < q )
A3: 0 / |.r.| = 0 ;
assume A4: 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 * g1)).| < q
then A5: 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 * g1)).| < q )
assume 0 < q ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
then consider n1 being Nat such that
A6: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < q / |.r.| by A1, A5, A3, XREAL_1:74;
take k = n1; :: thesis: for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
let m be 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 / |.r.| by A6;
A8: 0 < |.r.| by A4, COMPLEX1:47;
A9: |.r.| * (q / |.r.|) = |.r.| * ((|.r.| ") * q) by XCMPLX_0:def 9
.= (|.r.| * (|.r.| ")) * q
.= 1 * q by A8, XCMPLX_0:def 7
.= q ;
|.(((r * seq) . m) - (r * g1)).| = |.((r * (seq . m)) - (r * g1)).| by Th5
.= |.(r * ((seq . m) - g1)).| by RLVECT_1:34
.= |.r.| * |.((seq . m) - g1).| by Th7 ;
hence |.(((r * seq) . m) - (r * g1)).| < q by A5, A7, A9, XREAL_1:68; :: thesis: verum
end;
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 * g1)).| < q )
assume A10: 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 * g1)).| < 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 * g1)).| < q )
assume A11: 0 < q ; :: thesis: ex k being Nat st
for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
reconsider k = 0 as Nat ;
take k = k; :: thesis: for m being Nat st k <= m holds
|.(((r * seq) . m) - (r * g1)).| < q
let m be 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, RLVECT_1:10
.= |.((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 * (seq . m)).| by Th5
.= |.(0. (TOP-REAL N)).| by RLVECT_1:10
.= 0 by Th23 ;
hence |.(((r * seq) . m) - (r * g1)).| < q by A11; :: thesis: verum
end;
hence r * seq is convergent by A2; :: thesis: verum