let a be Real; :: thesis: for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)

let s1, s2 be Real_Sequence; :: thesis: ( a >= 1 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) implies lim s2 = a #R (lim s1) )
assume that
A1: a >= 1 and
A2: s1 is convergent and
A3: s2 is convergent and
A4: for n being Nat holds s2 . n = a #R (s1 . n) ; :: thesis: lim s2 = a #R (lim s1)
set d = |.(lim s1).| + 1;
A5: |.(lim s1).| < |.(lim s1).| + 1 by XREAL_1:29;
now :: thesis: for c being Real st c > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
|.((s2 . m) - (a #R (lim s1))).| < c
lim s1 <= |.(lim s1).| by ABSVALUE:4;
then lim s1 <= |.(lim s1).| + 1 by ;
then A6: a #R (lim s1) <= a #R (|.(lim s1).| + 1) by ;
a #R (lim s1) > 0 by ;
then A7: |.(a #R (lim s1)).| <= a #R (|.(lim s1).| + 1) by ;
A8: a #R (|.(lim s1).| + 1) >= 0 by ;
let c be Real; :: thesis: ( c > 0 implies ex n being Nat st
for m being Nat st m >= n holds
|.((s2 . m) - (a #R (lim s1))).| < c )

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

consider m1 being Nat such that
A10: ((a #R (|.(lim s1).| + 1)) * (a - 1)) / c < m1 by SEQ_4:3;
m1 + 1 >= m1 by XREAL_1:29;
then ((a #R (|.(lim s1).| + 1)) * (a - 1)) / c < m1 + 1 by ;
then (((a #R (|.(lim s1).| + 1)) * (a - 1)) / c) * c < c * (m1 + 1) by ;
then (a #R (|.(lim s1).| + 1)) * (a - 1) < c * (m1 + 1) by ;
then ((a #R (|.(lim s1).| + 1)) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:74;
then ((a #R (|.(lim s1).| + 1)) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A11: ((a #R (|.(lim s1).| + 1)) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:87;
reconsider m3 = (m1 + 1) " as Rational ;
A12: |.(a #R (lim s1)).| >= 0 by COMPLEX1:46;
consider n being Nat such that
A13: for m being Nat st n <= m holds
|.((s1 . m) - (lim s1)).| < (m1 + 1) " by ;
take n = n; :: thesis: for m being Nat st m >= n holds
|.((s2 . m) - (a #R (lim s1))).| < c

let m be Nat; :: thesis: ( m >= n implies |.((s2 . m) - (a #R (lim s1))).| < c )
assume m >= n ; :: thesis: |.((s2 . m) - (a #R (lim s1))).| < c
then A14: |.((s1 . m) - (lim s1)).| <= (m1 + 1) " by A13;
A15: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by ;
then A16: (a #R (|.(lim s1).| + 1)) * (((m1 + 1) -Root a) - 1) <= (a #R (|.(lim s1).| + 1)) * ((a - 1) / (m1 + 1)) by ;
(s1 . m) - (lim s1) <= |.((s1 . m) - (lim s1)).| by ABSVALUE:4;
then (s1 . m) - (lim s1) <= (m1 + 1) " by ;
then a #R ((s1 . m) - (lim s1)) <= a #R m3 by ;
then a #R ((s1 . m) - (lim s1)) <= a #Q m3 by ;
then a #R ((s1 . m) - (lim s1)) <= (m1 + 1) -Root a by ;
then A17: (a #R ((s1 . m) - (lim s1))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
A18: a #R ((s1 . m) - (lim s1)) <> 0 by ;
A19: a #R ((s1 . m) - (lim s1)) > 0 by ;
A20: now :: thesis: |.((a #R ((s1 . m) - (lim s1))) - 1).| <= ((m1 + 1) -Root a) - 1
per cases ) - (lim s1) >= 0 or (s1 . m) - (lim s1) < 0 ) ;
suppose (s1 . m) - (lim s1) >= 0 ; :: thesis: |.((a #R ((s1 . m) - (lim s1))) - 1).| <= ((m1 + 1) -Root a) - 1
then a #R ((s1 . m) - (lim s1)) >= 1 by ;
then (a #R ((s1 . m) - (lim s1))) - 1 >= 0 by XREAL_1:48;
hence |.((a #R ((s1 . m) - (lim s1))) - 1).| <= ((m1 + 1) -Root a) - 1 by ; :: thesis: verum
end;
suppose A21: (s1 . m) - (lim s1) < 0 ; :: thesis: |.((a #R ((s1 . m) - (lim s1))) - 1).| <= ((m1 + 1) -Root a) - 1
A22: - ((s1 . m) - (lim s1)) <= |.(- ((s1 . m) - (lim s1))).| by ABSVALUE:4;
|.((s1 . m) - (lim s1)).| = |.(- ((s1 . m) - (lim s1))).| by COMPLEX1:52;
then - ((s1 . m) - (lim s1)) <= m3 by ;
then a #R (- ((s1 . m) - (lim s1))) <= a #R m3 by ;
then a #R (- ((s1 . m) - (lim s1))) <= a #Q m3 by ;
then a #R (- ((s1 . m) - (lim s1))) <= (m1 + 1) -Root a by ;
then A23: (a #R (- ((s1 . m) - (lim s1)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:9;
a #R (- ((s1 . m) - (lim s1))) >= 1 by ;
then (a #R (- ((s1 . m) - (lim s1)))) - 1 >= 0 by XREAL_1:48;
then A24: |.((a #R (- ((s1 . m) - (lim s1)))) - 1).| <= ((m1 + 1) -Root a) - 1 by ;
a #R ((s1 . m) - (lim s1)) <= 1 by ;
then A25: |.(a #R ((s1 . m) - (lim s1))).| <= 1 by ;
|.((a #R (- ((s1 . m) - (lim s1)))) - 1).| >= 0 by COMPLEX1:46;
then A26: |.(a #R ((s1 . m) - (lim s1))).| * |.((a #R (- ((s1 . m) - (lim s1)))) - 1).| <= 1 * |.((a #R (- ((s1 . m) - (lim s1)))) - 1).| by ;
|.((a #R ((s1 . m) - (lim s1))) - 1).| = |.(((a #R ((s1 . m) - (lim s1))) - 1) * 1).|
.= |.(((a #R ((s1 . m) - (lim s1))) - 1) * ((a #R ((s1 . m) - (lim s1))) / (a #R ((s1 . m) - (lim s1))))).| by
.= |.(((a #R ((s1 . m) - (lim s1))) * ((a #R ((s1 . m) - (lim s1))) - 1)) / (a #R ((s1 . m) - (lim s1)))).|
.= |.((a #R ((s1 . m) - (lim s1))) * (((a #R ((s1 . m) - (lim s1))) - 1) / (a #R ((s1 . m) - (lim s1))))).|
.= |.(a #R ((s1 . m) - (lim s1))).| * |.(((a #R ((s1 . m) - (lim s1))) - 1) / (a #R ((s1 . m) - (lim s1)))).| by COMPLEX1:65
.= |.(a #R ((s1 . m) - (lim s1))).| * |.(((a #R ((s1 . m) - (lim s1))) / (a #R ((s1 . m) - (lim s1)))) - (1 / (a #R ((s1 . m) - (lim s1))))).|
.= |.(a #R ((s1 . m) - (lim s1))).| * |.(1 - (1 / (a #R ((s1 . m) - (lim s1))))).| by
.= |.(a #R ((s1 . m) - (lim s1))).| * |.(1 - (a #R (- ((s1 . m) - (lim s1))))).| by
.= |.(a #R ((s1 . m) - (lim s1))).| * |.(- (1 - (a #R (- ((s1 . m) - (lim s1)))))).| by COMPLEX1:52
.= |.(a #R ((s1 . m) - (lim s1))).| * |.((a #R (- ((s1 . m) - (lim s1)))) - 1).| ;
hence |.((a #R ((s1 . m) - (lim s1))) - 1).| <= ((m1 + 1) -Root a) - 1 by ; :: thesis: verum
end;
end;
end;
|.((a #R ((s1 . m) - (lim s1))) - 1).| >= 0 by COMPLEX1:46;
then A27: |.(a #R (lim s1)).| * |.((a #R ((s1 . m) - (lim s1))) - 1).| <= (a #R (|.(lim s1).| + 1)) * (((m1 + 1) -Root a) - 1) by ;
|.((a #R (s1 . m)) - (a #R (lim s1))).| = |.(((a #R (s1 . m)) - (a #R (lim s1))) * 1).|
.= |.(((a #R (s1 . m)) - (a #R (lim s1))) * ((a #R (lim s1)) / (a #R (lim s1)))).| by
.= |.(((a #R (lim s1)) * ((a #R (s1 . m)) - (a #R (lim s1)))) / (a #R (lim s1))).|
.= |.((a #R (lim s1)) * (((a #R (s1 . m)) - (a #R (lim s1))) / (a #R (lim s1)))).|
.= |.(a #R (lim s1)).| * |.(((a #R (s1 . m)) - (a #R (lim s1))) / (a #R (lim s1))).| by COMPLEX1:65
.= |.(a #R (lim s1)).| * |.(((a #R (s1 . m)) / (a #R (lim s1))) - ((a #R (lim s1)) / (a #R (lim s1)))).|
.= |.(a #R (lim s1)).| * |.(((a #R (s1 . m)) / (a #R (lim s1))) - 1).| by
.= |.(a #R (lim s1)).| * |.((a #R ((s1 . m) - (lim s1))) - 1).| by ;
then |.((a #R (s1 . m)) - (a #R (lim s1))).| <= ((a #R (|.(lim s1).| + 1)) * (a - 1)) / (m1 + 1) by ;
then |.((a #R (s1 . m)) - (a #R (lim s1))).| < c by ;
hence |.((s2 . m) - (a #R (lim s1))).| < c by A4; :: thesis: verum
end;
hence lim s2 = a #R (lim s1) by ; :: thesis: verum