let a be Real; :: thesis: for s being Rational_Sequence st s is convergent & a > 0 holds
a #Q s is convergent
let s be Rational_Sequence; :: thesis: ( s is convergent & a > 0 implies a #Q s is convergent )
assume that
A1: s is convergent and
A2: a > 0 ; :: thesis: a #Q s is convergent

per cases ( a >= 1 or a < 1 ) ;

suppose a >= 1 ; :: thesis: a #Q s is convergent

hence a #Q s is convergent by A1, Lm6; :: thesis: verum

end;

suppose A3: a < 1 ; :: thesis: a #Q s is convergent

then a / a < 1 / a by A2, XREAL_1:74;
then 1 < 1 / a by A2, XCMPLX_1:60;
then A4: (1 / a) #Q s is convergent by A1, Lm6;
s is bounded by A1;
then consider d being Real such that
0 < d and
A5: for n being Nat holds |.(s . n).| < d by SEQ_2:3;
reconsider d = d as Real ;
consider m1 being Nat such that
A6: 2 * d < m1 by SEQ_4:3;
reconsider m1 = m1 as Rational ;
A7: a #Q m1 > 0 by A2, Th52;

now :: thesis: for c being Real st c > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
|.(((a #Q s) . m) - ((a #Q s) . n)).| < c

let c be Real; :: thesis: ( c > 0 implies ex n being Nat st
for m being Nat st m >= n holds
|.(((a #Q s) . m) - ((a #Q s) . n)).| < c )
assume A8: c > 0 ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
|.(((a #Q s) . m) - ((a #Q s) . n)).| < c
then c * (a #Q m1) > 0 by A7;
then consider n being Nat such that
A9: for m being Nat st n <= m holds
|.((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)).| < c * (a #Q m1) by A4, SEQ_4:41;
take n = n; :: thesis: for m being Nat st m >= n holds
|.(((a #Q s) . m) - ((a #Q s) . n)).| < c
let m be Nat; :: thesis: ( m >= n implies |.(((a #Q s) . m) - ((a #Q s) . n)).| < c )
assume m >= n ; :: thesis: |.(((a #Q s) . m) - ((a #Q s) . n)).| < c
then A10: |.((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)).| < c * (a #Q m1) by A9;
A11: a #Q (s . m) <> 0 by A2, Th52;
A12: a #Q ((s . m) + (s . n)) > 0 by A2, Th52;
|.(s . m).| < d by A5;
then A13: |.(s . m).| + |.(s . n).| < d + d by A5, XREAL_1:8;
|.((s . m) + (s . n)).| <= |.(s . m).| + |.(s . n).| by COMPLEX1:56;
then |.((s . m) + (s . n)).| < d + d by A13, XXREAL_0:2;
then |.((s . m) + (s . n)).| < m1 by A6, XXREAL_0:2;
then A14: |.(- ((s . m) + (s . n))).| < m1 by COMPLEX1:52;
- ((s . m) + (s . n)) <= |.(- ((s . m) + (s . n))).| by ABSVALUE:4;
then - ((s . m) + (s . n)) < m1 by A14, XXREAL_0:2;
then A15: m1 - (- ((s . m) + (s . n))) > 0 by XREAL_1:50;
A16: a #Q (s . n) <> 0 by A2, Th52;
|.((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)).| = |.(((1 / a) #Q (s . m)) - (((1 / a) #Q s) . n)).| by Def5
.= |.(((1 / a) #Q (s . m)) - ((1 / a) #Q (s . n))).| by Def5
.= |.((1 / (a #Q (s . m))) - ((1 / a) #Q (s . n))).| by A2, Th57
.= |.((1 / (a #Q (s . m))) - (1 / (a #Q (s . n)))).| by A2, Th57
.= |.(((a #Q (s . m)) ") - (1 / (a #Q (s . n)))).|
.= |.(((a #Q (s . m)) ") - ((a #Q (s . n)) ")).|
.= |.((a #Q (s . m)) - (a #Q (s . n))).| / (|.(a #Q (s . m)).| * |.(a #Q (s . n)).|) by A11, A16, SEQ_2:2
.= |.((a #Q (s . m)) - (a #Q (s . n))).| / |.((a #Q (s . m)) * (a #Q (s . n))).| by COMPLEX1:65
.= |.((a #Q (s . m)) - (a #Q (s . n))).| / |.(a #Q ((s . m) + (s . n))).| by A2, Th53
.= |.((a #Q (s . m)) - (a #Q (s . n))).| / (a #Q ((s . m) + (s . n))) by A12, ABSVALUE:def 1 ;
then A17: (|.((a #Q (s . m)) - (a #Q (s . n))).| / (a #Q ((s . m) + (s . n)))) * (a #Q ((s . m) + (s . n))) < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by A10, A12, XREAL_1:68;
a #Q ((s . m) + (s . n)) <> 0 by A2, Th52;
then A18: |.((a #Q (s . m)) - (a #Q (s . n))).| < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by A17, XCMPLX_1:87;
(a #Q m1) * (a #Q ((s . m) + (s . n))) = a #Q (m1 + ((s . m) + (s . n))) by A2, Th53;
then c * ((a #Q m1) * (a #Q ((s . m) + (s . n)))) < 1 * c by A2, A3, A8, A15, Th65, XREAL_1:68;
then |.((a #Q (s . m)) - (a #Q (s . n))).| < c by A18, XXREAL_0:2;
then |.(((a #Q s) . m) - (a #Q (s . n))).| < c by Def5;
hence |.(((a #Q s) . m) - ((a #Q s) . n)).| < c by Def5; :: thesis: verum

end;

hence a #Q s is convergent by SEQ_4:41; :: thesis: verum

end;

end;