let s1, s2 be Rational_Sequence; :: thesis: for a being Real st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
lim (a #Q s1) = lim (a #Q s2)

let a be Real; :: thesis: ( s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 implies lim (a #Q s1) = lim (a #Q s2) )
assume that
A1: s1 is convergent and
A2: s2 is convergent and
A3: lim s1 = lim s2 and
A4: a >= 1 ; :: thesis: lim (a #Q s1) = lim (a #Q s2)
A5: s1 - s2 is convergent by A1, A2;
A6: a #Q s2 is convergent by A2, A4, Th69;
A7: now :: thesis: for n being Element of NAT holds (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (a #Q s1) . n
let n be Element of NAT ; :: thesis: (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (a #Q s1) . n
thus (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (((a #Q s1) - (a #Q s2)) . n) + ((a #Q s2) . n) by SEQ_1:7
.= (((a #Q s1) . n) - ((a #Q s2) . n)) + ((a #Q s2) . n) by RFUNCT_2:1
.= (a #Q s1) . n ; :: thesis: verum
end;
s2 is bounded by A2;
then consider d being Real such that
0 < d and
A8: for n being Nat holds |.(s2 . n).| < d by SEQ_2:3;
consider m2 being Nat such that
A9: d < m2 by SEQ_4:3;
reconsider m2 = m2 as Rational ;
A10: lim (s1 - s2) = (lim s1) - (lim s2) by
.= 0 by A3 ;
A11: 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 s1) - (a #Q s2)) . m) - 0).| < c
A12: 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 s1) - (a #Q s2)) . m) - 0).| < c )

assume A13: c > 0 ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c

consider m1 being Nat such that
A14: ((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 A15: ((a #Q m2) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:87;
consider n being Nat such that
A16: for m being Nat st n <= m holds
|.(((s1 - s2) . m) - 0).| < (m1 + 1) " by ;
take n = n; :: thesis: for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c

let m be Nat; :: thesis: ( m >= n implies |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c )
assume m >= n ; :: thesis: |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c
then |.(((s1 - s2) . m) - 0).| < (m1 + 1) " by A16;
then A17: |.((s1 . m) - (s2 . m)).| <= (m1 + 1) " by RFUNCT_2:1;
A18: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by ;
then A19: (a #Q m2) * (((m1 + 1) -Root a) - 1) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by ;
A20: a #Q (s2 . m) <> 0 by ;
A21: |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| = |.(((a #Q (s1 . m)) - (a #Q (s2 . m))) * 1).|
.= |.(((a #Q (s1 . m)) - (a #Q (s2 . m))) * ((a #Q (s2 . m)) / (a #Q (s2 . m)))).| by
.= |.(((a #Q (s2 . m)) * ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q (s2 . m))).|
.= |.((a #Q (s2 . m)) * (((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m)))).|
.= |.(a #Q (s2 . m)).| * |.(((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m))).| by COMPLEX1:65
.= |.(a #Q (s2 . m)).| * |.(((a #Q (s1 . m)) / (a #Q (s2 . m))) - ((a #Q (s2 . m)) / (a #Q (s2 . m)))).|
.= |.(a #Q (s2 . m)).| * |.(((a #Q (s1 . m)) / (a #Q (s2 . m))) - 1).| by
.= |.(a #Q (s2 . m)).| * |.((a #Q ((s1 . m) - (s2 . m))) - 1).| by ;
A22: s2 . m <= |.(s2 . m).| by ABSVALUE:4;
reconsider m3 = (m1 + 1) " as Rational ;
A23: |.((a #Q ((s1 . m) - (s2 . m))) - 1).| >= 0 by COMPLEX1:46;
A24: a #Q ((s1 . m) - (s2 . m)) <> 0 by ;
(s1 . m) - (s2 . m) <= |.((s1 . m) - (s2 . m)).| by ABSVALUE:4;
then (s1 . m) - (s2 . m) <= (m1 + 1) " by ;
then a #Q ((s1 . m) - (s2 . m)) <= a #Q m3 by ;
then a #Q ((s1 . m) - (s2 . m)) <= (m1 + 1) -Root a by ;
then A25: (a #Q ((s1 . m) - (s2 . m))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
A26: a #Q ((s1 . m) - (s2 . m)) > 0 by ;
A27: now :: thesis: |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= ((m1 + 1) -Root a) - 1
per cases ) - (s2 . m) >= 0 or (s1 . m) - (s2 . m) < 0 ) ;
suppose (s1 . m) - (s2 . m) >= 0 ; :: thesis: |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= ((m1 + 1) -Root a) - 1
then a #Q ((s1 . m) - (s2 . m)) >= 1 by ;
then (a #Q ((s1 . m) - (s2 . m))) - 1 >= 0 by XREAL_1:48;
hence |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= ((m1 + 1) -Root a) - 1 by ; :: thesis: verum
end;
suppose A28: (s1 . m) - (s2 . m) < 0 ; :: thesis: |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= ((m1 + 1) -Root a) - 1
A29: - ((s1 . m) - (s2 . m)) <= |.(- ((s1 . m) - (s2 . m))).| by ABSVALUE:4;
|.((s1 . m) - (s2 . m)).| = |.(- ((s1 . m) - (s2 . m))).| by COMPLEX1:52;
then - ((s1 . m) - (s2 . m)) <= m3 by ;
then a #Q (- ((s1 . m) - (s2 . m))) <= a #Q m3 by ;
then a #Q (- ((s1 . m) - (s2 . m))) <= (m1 + 1) -Root a by ;
then A30: (a #Q (- ((s1 . m) - (s2 . m)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
a #Q (- ((s1 . m) - (s2 . m))) >= 1 by ;
then (a #Q (- ((s1 . m) - (s2 . m)))) - 1 >= 0 by XREAL_1:48;
then A31: |.((a #Q (- ((s1 . m) - (s2 . m)))) - 1).| <= ((m1 + 1) -Root a) - 1 by ;
a #Q ((s1 . m) - (s2 . m)) <= 1 by ;
then A32: |.(a #Q ((s1 . m) - (s2 . m))).| <= 1 by ;
|.((a #Q (- ((s1 . m) - (s2 . m)))) - 1).| >= 0 by COMPLEX1:46;
then A33: |.(a #Q ((s1 . m) - (s2 . m))).| * |.((a #Q (- ((s1 . m) - (s2 . m)))) - 1).| <= 1 * |.((a #Q (- ((s1 . m) - (s2 . m)))) - 1).| by ;
|.((a #Q ((s1 . m) - (s2 . m))) - 1).| = |.(((a #Q ((s1 . m) - (s2 . m))) - 1) * 1).|
.= |.(((a #Q ((s1 . m) - (s2 . m))) - 1) * ((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m))))).| by
.= |.(((a #Q ((s1 . m) - (s2 . m))) * ((a #Q ((s1 . m) - (s2 . m))) - 1)) / (a #Q ((s1 . m) - (s2 . m)))).|
.= |.((a #Q ((s1 . m) - (s2 . m))) * (((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m))))).|
.= |.(a #Q ((s1 . m) - (s2 . m))).| * |.(((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m)))).| by COMPLEX1:65
.= |.(a #Q ((s1 . m) - (s2 . m))).| * |.(((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m)))) - (1 / (a #Q ((s1 . m) - (s2 . m))))).|
.= |.(a #Q ((s1 . m) - (s2 . m))).| * |.(1 - (1 / (a #Q ((s1 . m) - (s2 . m))))).| by
.= |.(a #Q ((s1 . m) - (s2 . m))).| * |.(1 - (a #Q (- ((s1 . m) - (s2 . m))))).| by
.= |.(a #Q ((s1 . m) - (s2 . m))).| * |.(- (1 - (a #Q (- ((s1 . m) - (s2 . m)))))).| by COMPLEX1:52
.= |.(a #Q ((s1 . m) - (s2 . m))).| * |.((a #Q (- ((s1 . m) - (s2 . m)))) - 1).| ;
hence |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= ((m1 + 1) -Root a) - 1 by ; :: thesis: verum
end;
end;
end;
A34: a #Q (s2 . m) > 0 by ;
|.(s2 . m).| <= m2 by ;
then s2 . m <= m2 by ;
then a #Q (s2 . m) <= a #Q m2 by ;
then A35: |.(a #Q (s2 . m)).| <= a #Q m2 by ;
|.(a #Q (s2 . m)).| >= 0 by ;
then |.(a #Q (s2 . m)).| * |.((a #Q ((s1 . m) - (s2 . m))) - 1).| <= (a #Q m2) * (((m1 + 1) -Root a) - 1) by ;
then |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| <= ((a #Q m2) * (a - 1)) / (m1 + 1) by ;
then |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < c by ;
then |.(((a #Q s1) . m) - (a #Q (s2 . m))).| < c by Def5;
then |.(((a #Q s1) . m) - ((a #Q s2) . m)).| < c by Def5;
hence |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c by RFUNCT_2:1; :: thesis: verum
end;
then A36: (a #Q s1) - (a #Q s2) is convergent by SEQ_2:def 6;
then lim ((a #Q s1) - (a #Q s2)) = 0 by ;
then lim (((a #Q s1) - (a #Q s2)) + (a #Q s2)) = 0 + (lim (a #Q s2)) by
.= lim (a #Q s2) ;
hence lim (a #Q s1) = lim (a #Q s2) by ; :: thesis: verum