let s be Rational_Sequence; :: thesis: for a being Real st s is convergent & a >= 1 holds
a #Q s is convergent

let a be Real; :: 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;
then consider d being Real such that
0 < d and
A3: for n being Nat holds |.(s . n).| < d by SEQ_2:3;
consider m2 being Nat such that
A4: d < m2 by SEQ_4:3;
reconsider m2 = m2 as Rational ;
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
A5: a #Q m2 >= 0 by ;
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 A6: 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

consider m1 being Nat such that
A7: ((a #Q m2) * (a - 1)) / c < m1 by SEQ_4:3;
m1 + 1 >= m1 by XREAL_1:29;
then ((a #Q m2) * (a - 1)) / c < m1 + 1 by ;
then (((a #Q m2) * (a - 1)) / c) * c < c * (m1 + 1) by ;
then (a #Q m2) * (a - 1) < c * (m1 + 1) by ;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:74;
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:87;
consider n being Nat such that
A9: for m being Nat st n <= m holds
|.((s . m) - (s . n)).| < (m1 + 1) " 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: |.((s . m) - (s . n)).| <= (m1 + 1) " by A9;
A11: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by ;
then A12: (a #Q m2) * (((m1 + 1) -Root a) - 1) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by ;
A13: a #Q (s . n) <> 0 by ;
A14: |.((a #Q (s . m)) - (a #Q (s . n))).| = |.(((a #Q (s . m)) - (a #Q (s . n))) * 1).|
.= |.(((a #Q (s . m)) - (a #Q (s . n))) * ((a #Q (s . n)) / (a #Q (s . n)))).| by
.= |.(((a #Q (s . n)) * ((a #Q (s . m)) - (a #Q (s . n)))) / (a #Q (s . n))).|
.= |.((a #Q (s . n)) * (((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n)))).|
.= |.(a #Q (s . n)).| * |.(((a #Q (s . m)) - (a #Q (s . n))) / (a #Q (s . n))).| by COMPLEX1:65
.= |.(a #Q (s . n)).| * |.(((a #Q (s . m)) / (a #Q (s . n))) - ((a #Q (s . n)) / (a #Q (s . n)))).|
.= |.(a #Q (s . n)).| * |.(((a #Q (s . m)) / (a #Q (s . n))) - 1).| by
.= |.(a #Q (s . n)).| * |.((a #Q ((s . m) - (s . n))) - 1).| by ;
A15: s . n <= |.(s . n).| by ABSVALUE:4;
reconsider m3 = (m1 + 1) " as Rational ;
A16: |.((a #Q ((s . m) - (s . n))) - 1).| >= 0 by COMPLEX1:46;
A17: a #Q ((s . m) - (s . n)) <> 0 by ;
(s . m) - (s . n) <= |.((s . m) - (s . n)).| by ABSVALUE:4;
then (s . m) - (s . n) <= (m1 + 1) " by ;
then a #Q ((s . m) - (s . n)) <= a #Q m3 by ;
then a #Q ((s . m) - (s . n)) <= (m1 + 1) -Root a by ;
then A18: (a #Q ((s . m) - (s . n))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
A19: a #Q ((s . m) - (s . n)) > 0 by ;
A20: now :: thesis: |.((a #Q ((s . m) - (s . n))) - 1).| <= ((m1 + 1) -Root a) - 1
per cases ) - (s . n) >= 0 or (s . m) - (s . n) < 0 ) ;
suppose (s . m) - (s . n) >= 0 ; :: thesis: |.((a #Q ((s . m) - (s . n))) - 1).| <= ((m1 + 1) -Root a) - 1
then a #Q ((s . m) - (s . n)) >= 1 by ;
then (a #Q ((s . m) - (s . n))) - 1 >= 0 by XREAL_1:48;
hence |.((a #Q ((s . m) - (s . n))) - 1).| <= ((m1 + 1) -Root a) - 1 by ; :: thesis: verum
end;
suppose A21: (s . m) - (s . n) < 0 ; :: thesis: |.((a #Q ((s . m) - (s . n))) - 1).| <= ((m1 + 1) -Root a) - 1
A22: - ((s . m) - (s . n)) <= |.(- ((s . m) - (s . n))).| by ABSVALUE:4;
|.((s . m) - (s . n)).| = |.(- ((s . m) - (s . n))).| by COMPLEX1:52;
then - ((s . m) - (s . n)) <= m3 by ;
then a #Q (- ((s . m) - (s . n))) <= a #Q m3 by ;
then a #Q (- ((s . m) - (s . n))) <= (m1 + 1) -Root a by ;
then A23: (a #Q (- ((s . m) - (s . n)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
a #Q (- ((s . m) - (s . n))) >= 1 by ;
then (a #Q (- ((s . m) - (s . n)))) - 1 >= 0 by XREAL_1:48;
then A24: |.((a #Q (- ((s . m) - (s . n)))) - 1).| <= ((m1 + 1) -Root a) - 1 by ;
a #Q ((s . m) - (s . n)) <= 1 by ;
then A25: |.(a #Q ((s . m) - (s . n))).| <= 1 by ;
|.((a #Q (- ((s . m) - (s . n)))) - 1).| >= 0 by COMPLEX1:46;
then A26: |.(a #Q ((s . m) - (s . n))).| * |.((a #Q (- ((s . m) - (s . n)))) - 1).| <= 1 * |.((a #Q (- ((s . m) - (s . n)))) - 1).| by ;
|.((a #Q ((s . m) - (s . n))) - 1).| = |.(((a #Q ((s . m) - (s . n))) - 1) * 1).|
.= |.(((a #Q ((s . m) - (s . n))) - 1) * ((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n))))).| by
.= |.(((a #Q ((s . m) - (s . n))) * ((a #Q ((s . m) - (s . n))) - 1)) / (a #Q ((s . m) - (s . n)))).|
.= |.((a #Q ((s . m) - (s . n))) * (((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n))))).|
.= |.(a #Q ((s . m) - (s . n))).| * |.(((a #Q ((s . m) - (s . n))) - 1) / (a #Q ((s . m) - (s . n)))).| by COMPLEX1:65
.= |.(a #Q ((s . m) - (s . n))).| * |.(((a #Q ((s . m) - (s . n))) / (a #Q ((s . m) - (s . n)))) - (1 / (a #Q ((s . m) - (s . n))))).|
.= |.(a #Q ((s . m) - (s . n))).| * |.(1 - (1 / (a #Q ((s . m) - (s . n))))).| by
.= |.(a #Q ((s . m) - (s . n))).| * |.(1 - (a #Q (- ((s . m) - (s . n))))).| by
.= |.(a #Q ((s . m) - (s . n))).| * |.(- (1 - (a #Q (- ((s . m) - (s . n)))))).| by COMPLEX1:52
.= |.(a #Q ((s . m) - (s . n))).| * |.((a #Q (- ((s . m) - (s . n)))) - 1).| ;
hence |.((a #Q ((s . m) - (s . n))) - 1).| <= ((m1 + 1) -Root a) - 1 by ; :: thesis: verum
end;
end;
end;
A27: a #Q (s . n) > 0 by ;
|.(s . n).| <= m2 by ;
then s . n <= m2 by ;
then a #Q (s . n) <= a #Q m2 by ;
then A28: |.(a #Q (s . n)).| <= a #Q m2 by ;
|.(a #Q (s . n)).| >= 0 by ;
then |.(a #Q (s . n)).| * |.((a #Q ((s . m) - (s . n))) - 1).| <= (a #Q m2) * (((m1 + 1) -Root a) - 1) by ;
then |.((a #Q (s . m)) - (a #Q (s . n))).| <= ((a #Q m2) * (a - 1)) / (m1 + 1) 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