let a be real number ; :: 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:76;
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, SEQ_2:27;
then consider d being real number such that
0 < d and
A5: for n being Element of NAT holds abs (s . n) < d by SEQ_2:15;
reconsider d = d as Real by XREAL_0:def 1;
consider m1 being Element of NAT such that
A6: 2 * d < m1 by SEQ_4:10;
reconsider m1 = m1 as Rational ;
A7: a #Q m1 > 0 by A2, Th63;

now

let c be real number ; :: thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c )
assume A8: c > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c
then c * (a #Q m1) > 0 by A7, XREAL_1:131;
then consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) < c * (a #Q m1) by A4, SEQ_4:58;
take n = n; :: thesis: for m being Element of NAT st m >= n holds
abs (((a #Q s) . m) - ((a #Q s) . n)) < c
let m be Element of NAT ; :: thesis: ( m >= n implies abs (((a #Q s) . m) - ((a #Q s) . n)) < c )
assume m >= n ; :: thesis: abs (((a #Q s) . m) - ((a #Q s) . n)) < c
then A10: abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) < c * (a #Q m1) by A9;
A11: a #Q (s . m) <> 0 by A2, Th63;
A12: a #Q ((s . m) + (s . n)) > 0 by A2, Th63;
abs (s . m) < d by A5;
then A13: (abs (s . m)) + (abs (s . n)) < d + d by A5, XREAL_1:10;
abs ((s . m) + (s . n)) <= (abs (s . m)) + (abs (s . n)) by COMPLEX1:142;
then abs ((s . m) + (s . n)) < d + d by A13, XXREAL_0:2;
then abs ((s . m) + (s . n)) < m1 by A6, XXREAL_0:2;
then A14: abs (- ((s . m) + (s . n))) < m1 by COMPLEX1:138;
- ((s . m) + (s . n)) <= abs (- ((s . m) + (s . n))) by ABSVALUE:11;
then - ((s . m) + (s . n)) < m1 by A14, XXREAL_0:2;
then A15: m1 - (- ((s . m) + (s . n))) > 0 by XREAL_1:52;
A16: a #Q (s . n) <> 0 by A2, Th63;
abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) = abs (((1 / a) #Q (s . m)) - (((1 / a) #Q s) . n)) by Def7
.= abs (((1 / a) #Q (s . m)) - ((1 / a) #Q (s . n))) by Def7
.= abs ((1 / (a #Q (s . m))) - ((1 / a) #Q (s . n))) by A2, Th68
.= abs ((1 / (a #Q (s . m))) - (1 / (a #Q (s . n)))) by A2, Th68
.= abs (((a #Q (s . m)) " ) - (1 / (a #Q (s . n))))
.= abs (((a #Q (s . m)) " ) - ((a #Q (s . n)) " ))
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / ((abs (a #Q (s . m))) * (abs (a #Q (s . n)))) by A11, A16, SEQ_2:11
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (abs ((a #Q (s . m)) * (a #Q (s . n)))) by COMPLEX1:151
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (abs (a #Q ((s . m) + (s . n)))) by A2, Th64
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q ((s . m) + (s . n))) by A12, ABSVALUE:def 1 ;
then A17: ((abs ((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:70;
a #Q ((s . m) + (s . n)) <> 0 by A2, Th63;
then A18: abs ((a #Q (s . m)) - (a #Q (s . n))) < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by A17, XCMPLX_1:88;
(a #Q m1) * (a #Q ((s . m) + (s . n))) = a #Q (m1 + ((s . m) + (s . n))) by A2, Th64;
then c * ((a #Q m1) * (a #Q ((s . m) + (s . n)))) < 1 * c by A2, A3, A8, A15, Th76, XREAL_1:70;
then abs ((a #Q (s . m)) - (a #Q (s . n))) < c by A18, XXREAL_0:2;
then abs (((a #Q s) . m) - (a #Q (s . n))) < c by Def7;
hence abs (((a #Q s) . m) - ((a #Q s) . n)) < c by Def7; :: thesis: verum

end;

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

end;

end;