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 A1: ( s is convergent & 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, Lm5; :: thesis: verum

end;

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

then a / a < 1 / a by A1, XREAL_1:76;
then 1 < 1 / a by A1, XCMPLX_1:60;
then A3: (1 / a) #Q s is convergent by A1, Lm5;
s is bounded by A1, SEQ_2:27;
then consider d being real number such that
A4: ( 0 < d & ( 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
A5: 2 * d < m1 by SEQ_4:10;
reconsider m1 = m1 as Rational ;
A6: a #Q m1 > 0 by A1, 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 A7: 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 A6, XREAL_1:131;
then consider n being Element of NAT such that
A8: 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 A3, 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 A9: abs ((((1 / a) #Q s) . m) - (((1 / a) #Q s) . n)) < c * (a #Q m1) by A8;
A10: a #Q (s . m) <> 0 by A1, Th63;
A11: a #Q (s . n) <> 0 by A1, Th63;
A12: a #Q ((s . m) + (s . n)) > 0 by A1, Th63;
A13: a #Q ((s . m) + (s . n)) <> 0 by A1, 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 A1, Th68
.= abs ((1 / (a #Q (s . m))) - (1 / (a #Q (s . n)))) by A1, 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 A10, A11, 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 A1, Th64
.= (abs ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q ((s . m) + (s . n))) by A12, ABSVALUE:def 1 ;
then ((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 A9, A12, XREAL_1:70;
then A14: abs ((a #Q (s . m)) - (a #Q (s . n))) < (c * (a #Q m1)) * (a #Q ((s . m) + (s . n))) by A13, XCMPLX_1:88;
abs (s . m) < d by A4;
then A15: (abs (s . m)) + (abs (s . n)) < d + d by A4, 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 A15, XXREAL_0:2;
then abs ((s . m) + (s . n)) < m1 by A5, XXREAL_0:2;
then A16: 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 A16, XXREAL_0:2;
then A17: m1 - (- ((s . m) + (s . n))) > 0 by XREAL_1:52;
(a #Q m1) * (a #Q ((s . m) + (s . n))) = a #Q (m1 + ((s . m) + (s . n))) by A1, Th64;
then c * ((a #Q m1) * (a #Q ((s . m) + (s . n)))) < 1 * c by A1, A2, A7, A17, Th76, XREAL_1:70;
then abs ((a #Q (s . m)) - (a #Q (s . n))) < c by A14, 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;