let s be Rational_Sequence; :: thesis: for a being real number st s is convergent & a >= 1 holds
a #Q s is convergent
let a be real number ; :: thesis: ( s is convergent & a >= 1 implies a #Q s is convergent )
assume that
A1: s is convergent and
A2: a >= 1 ; :: thesis: a #Q s is convergent
s is bounded by A1, SEQ_2:27;
then consider d being real number such that
A3: ( 0 < d & ( for n being Element of NAT holds abs (s . n) < d ) ) by SEQ_2:15;
consider m2 being Element of NAT such that
A4: d < m2 by SEQ_4:10;
reconsider m2 = m2 as Rational ;

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 A5: 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
consider m1 being Element of NAT such that
A6: ((a #Q m2) * (a - 1)) / c < m1 by SEQ_4:10;
A7: m1 + 1 >= 0 + 1 by NAT_1:13;
m1 + 1 >= m1 by XREAL_1:31;
then ((a #Q m2) * (a - 1)) / c < m1 + 1 by A6, XXREAL_0:2;
then (((a #Q m2) * (a - 1)) / c) * c < c * (m1 + 1) by A5, XREAL_1:70;
then (a #Q m2) * (a - 1) < c * (m1 + 1) by A5, XCMPLX_1:88;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:76;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A8: ((a #Q m2) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:88;
consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
abs ((s . m) - (s . n)) < (m1 + 1) " by A1, 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 ((s . m) - (s . n)) <= (m1 + 1) " by A9;
(s . m) - (s . n) <= abs ((s . m) - (s . n)) by ABSVALUE:11;
then A11: (s . m) - (s . n) <= (m1 + 1) " by A10, XXREAL_0:2;
reconsider m3 = (m1 + 1) " as Rational ;
a #Q ((s . m) - (s . n)) <= a #Q m3 by A2, A11, Th74;
then a #Q ((s . m) - (s . n)) <= (m1 + 1) -Root a by A2, A7, Th61;
then A12: (a #Q ((s . m) - (s . n))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:11;
A13: a #Q ((s . m) - (s . n)) > 0 by A2, Th63;
A14: a #Q ((s . m) - (s . n)) <> 0 by A2, Th63;

A15: now

per cases ( (s . m) - (s . n) >= 0 or (s . m) - (s . n) < 0 ) ;

suppose (s . m) - (s . n) >= 0 ; :: thesis: abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1

then a #Q ((s . m) - (s . n)) >= 1 by A2, Th71;
then (a #Q ((s . m) - (s . n))) - 1 >= 0 by XREAL_1:50;
hence abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1 by A12, ABSVALUE:def 1; :: thesis: verum

end;

suppose A16: (s . m) - (s . n) < 0 ; :: thesis: abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1

then A17: - ((s . m) - (s . n)) >= 0 ;
a #Q ((s . m) - (s . n)) <= 1 by A2, A16, Th72;
then A18: abs (a #Q ((s . m) - (s . n))) <= 1 by A13, ABSVALUE:def 1;
A19: abs ((s . m) - (s . n)) = abs (- ((s . m) - (s . n))) by COMPLEX1:138;
- ((s . m) - (s . n)) <= abs (- ((s . m) - (s . n))) by ABSVALUE:11;
then - ((s . m) - (s . n)) <= m3 by A10, A19, XXREAL_0:2;
then a #Q (- ((s . m) - (s . n))) <= a #Q m3 by A2, Th74;
then a #Q (- ((s . m) - (s . n))) <= (m1 + 1) -Root a by A2, A7, Th61;
then A20: (a #Q (- ((s . m) - (s . n)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:11;
a #Q (- ((s . m) - (s . n))) >= 1 by A2, A17, Th71;
then (a #Q (- ((s . m) - (s . n)))) - 1 >= 0 by XREAL_1:50;
then A21: abs ((a #Q (- ((s . m) - (s . n)))) - 1) <= ((m1 + 1) -Root a) - 1 by A20, ABSVALUE:def 1;
A22: abs ((a #Q ((s . m) - (s . n))) - 1) = abs (((a #Q ((s . m) - (s . n))) - 1) * 1)
.= abs (((a #Q ((s . m) - (s . n))) - 1) * ((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n))))) by A14, XCMPLX_1:60
.= abs (((a #Q ((s . m) - (s . n))) * ((a #Q ((s . m) - (s . n))) - 1)) / (a #Q ((s . m) - (s . n))))
.= abs ((a #Q ((s . m) - (s . n))) * (((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n)))))
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n))))) by COMPLEX1:151
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n)))) - (1 / (a #Q ((s . m) - (s . n))))))
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (1 - (1 / (a #Q ((s . m) - (s . n)))))) by A14, XCMPLX_1:60
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (1 - (a #Q (- ((s . m) - (s . n)))))) by A2, Th65
.= (abs (a #Q ((s . m) - (s . n)))) * (abs (- (1 - (a #Q (- ((s . m) - (s . n))))))) by COMPLEX1:138
.= (abs (a #Q ((s . m) - (s . n)))) * (abs ((a #Q (- ((s . m) - (s . n)))) - 1)) ;
abs ((a #Q (- ((s . m) - (s . n)))) - 1) >= 0 by COMPLEX1:132;
then (abs (a #Q ((s . m) - (s . n)))) * (abs ((a #Q (- ((s . m) - (s . n)))) - 1)) <= 1 * (abs ((a #Q (- ((s . m) - (s . n)))) - 1)) by A18, XREAL_1:66;
hence abs ((a #Q ((s . m) - (s . n))) - 1) <= ((m1 + 1) -Root a) - 1 by A21, A22, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A23: abs ((a #Q ((s . m) - (s . n))) - 1) >= 0 by COMPLEX1:132;
A24: abs (s . n) <= m2 by A3, A4, XXREAL_0:2;
s . n <= abs (s . n) by ABSVALUE:11;
then s . n <= m2 by A24, XXREAL_0:2;
then A25: a #Q (s . n) <= a #Q m2 by A2, Th74;
A26: a #Q (s . n) > 0 by A2, Th63;
then A27: abs (a #Q (s . n)) >= 0 by ABSVALUE:def 1;
A28: a #Q (s . n) <> 0 by A2, Th63;
abs (a #Q (s . n)) <= a #Q m2 by A25, A26, ABSVALUE:def 1;
then A29: (abs (a #Q (s . n))) * (abs ((a #Q ((s . m) - (s . n))) - 1)) <= (a #Q m2) * (((m1 + 1) -Root a) - 1) by A15, A23, A27, XREAL_1:68;
A30: abs ((a #Q (s . m)) - (a #Q (s . n))) = abs (((a #Q (s . m)) - (a #Q (s . n))) * 1)
.= abs (((a #Q (s . m)) - (a #Q (s . n))) * ((a #Q (s . n)) / (a #Q (s . n)))) by A28, XCMPLX_1:60
.= abs (((a #Q (s . n)) * ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q (s . n)))
.= abs ((a #Q (s . n)) * (((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n))))
.= (abs (a #Q (s . n))) * (abs (((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n)))) by COMPLEX1:151
.= (abs (a #Q (s . n))) * (abs (((a #Q (s . m)) / (a #Q (s . n))) - ((a #Q (s . n)) / (a #Q (s . n)))))
.= (abs (a #Q (s . n))) * (abs (((a #Q (s . m)) / (a #Q (s . n))) - 1)) by A28, XCMPLX_1:60
.= (abs (a #Q (s . n))) * (abs ((a #Q ((s . m) - (s . n))) - 1)) by A2, Th66 ;
A31: ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by A2, A7, Th40;
a #Q m2 >= 0 by A2, Th63;
then (a #Q m2) * (((m1 + 1) -Root a) - 1) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by A31, XREAL_1:66;
then abs ((a #Q (s . m)) - (a #Q (s . n))) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by A29, A30, XXREAL_0:2;
then abs ((a #Q (s . m)) - (a #Q (s . n))) <= ((a #Q m2) * (a - 1)) / (m1 + 1) ;
then abs ((a #Q (s . m)) - (a #Q (s . n))) < c by A8, 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