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 ; :: thesis: verum
end;
suppose A3: a < 1 ; :: thesis: a #Q s is convergent
then a / a < 1 / a by ;
then 1 < 1 / a by ;
then A4: (1 / a) #Q s is convergent by ;
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 ;
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 ;
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 ;
A12: a #Q ((s . m) + (s . n)) > 0 by ;
|.(s . m).| < d by A5;
then A13: |.(s . m).| + |.(s . n).| < d + d by ;
|.((s . m) + (s . n)).| <= |.(s . m).| + |.(s . n).| by COMPLEX1:56;
then |.((s . m) + (s . n)).| < d + d by ;
then |.((s . m) + (s . n)).| < m1 by ;
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 ;
then A15: m1 - (- ((s . m) + (s . n))) > 0 by XREAL_1:50;
A16: a #Q (s . n) <> 0 by ;
|.((((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
.= |.((1 / (a #Q (s . m))) - (1 / (a #Q (s . n)))).| by
.= |.(((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
.= |.((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
.= |.((a #Q (s . m)) - (a #Q (s . n))).| / (a #Q ((s . m) + (s . n))) by ;
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 ;
a #Q ((s . m) + (s . n)) <> 0 by ;
then A18: |.((a #Q (s . m)) - (a #Q (s . n))).| < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by ;
(a #Q m1) * (a #Q ((s . m) + (s . n))) = a #Q (m1 + ((s . m) + (s . n))) by ;
then c * ((a #Q m1) * (a #Q ((s . m) + (s . n)))) < 1 * c by ;
then |.((a #Q (s . m)) - (a #Q (s . n))).| < c by ;
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;