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 A5, XXREAL_0:2;
then A6: a #R (lim s1) <= a #R (|.(lim s1).| + 1) by A1, Th82;
a #R (lim s1) > 0 by A1, Th81;
then A7: |.(a #R (lim s1)).| <= a #R (|.(lim s1).| + 1) by A6, ABSVALUE:def 1;
A8: a #R (|.(lim s1).| + 1) >= 0 by A1, Th81;
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 A10, XXREAL_0:2;
then (((a #R (|.(lim s1).| + 1)) * (a - 1)) / c) * c < c * (m1 + 1) by A9, XREAL_1:68;
then (a #R (|.(lim s1).| + 1)) * (a - 1) < c * (m1 + 1) by A9, XCMPLX_1:87;
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 A2, SEQ_2:def 7;
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 A1, Th31;
then A16: (a #R (|.(lim s1).| + 1)) * (((m1 + 1) -Root a) - 1) <= (a #R (|.(lim s1).| + 1)) * ((a - 1) / (m1 + 1)) by A8, XREAL_1:64;
(s1 . m) - (lim s1) <= |.((s1 . m) - (lim s1)).| by ABSVALUE:4;
then (s1 . m) - (lim s1) <= (m1 + 1) " by A14, XXREAL_0:2;
then a #R ((s1 . m) - (lim s1)) <= a #R m3 by A1, Th82;
then a #R ((s1 . m) - (lim s1)) <= a #Q m3 by A1, Th74;
then a #R ((s1 . m) - (lim s1)) <= (m1 + 1) -Root a by A15, Th50;
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 A1, Th81;
A19: a #R ((s1 . m) - (lim s1)) > 0 by A1, Th81;

A20: now :: thesis: |.((a #R ((s1 . m) - (lim s1))) - 1).| <= ((m1 + 1) -Root a) - 1

per cases ( (s1 . m) - (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 A1, Th85;
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 A17, ABSVALUE:def 1; :: 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 A14, A22, XXREAL_0:2;
then a #R (- ((s1 . m) - (lim s1))) <= a #R m3 by A1, Th82;
then a #R (- ((s1 . m) - (lim s1))) <= a #Q m3 by A1, Th74;
then a #R (- ((s1 . m) - (lim s1))) <= (m1 + 1) -Root a by A15, Th50;
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 A1, A21, Th85;
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 A23, ABSVALUE:def 1;
a #R ((s1 . m) - (lim s1)) <= 1 by A1, A21, Th87;
then A25: |.(a #R ((s1 . m) - (lim s1))).| <= 1 by A19, ABSVALUE:def 1;
|.((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 A25, XREAL_1:64;
|.((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 A18, XCMPLX_1:60
.= |.(((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 A18, XCMPLX_1:60
.= |.(a #R ((s1 . m) - (lim s1))).| * |.(1 - (a #R (- ((s1 . m) - (lim s1))))).| by A1, Th76
.= |.(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 A24, A26, XXREAL_0:2; :: 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 A20, A12, A7, XREAL_1:66;
|.((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 A1, Lm9, XCMPLX_1:60
.= |.(((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 A1, Lm9, XCMPLX_1:60
.= |.(a #R (lim s1)).| * |.((a #R ((s1 . m) - (lim s1))) - 1).| by A1, Th77 ;
then |.((a #R (s1 . m)) - (a #R (lim s1))).| <= ((a #R (|.(lim s1).| + 1)) * (a - 1)) / (m1 + 1) by A27, A16, XXREAL_0:2;
then |.((a #R (s1 . m)) - (a #R (lim s1))).| < c by A11, XXREAL_0:2;
hence |.((s2 . m) - (a #R (lim s1))).| < c by A4; :: thesis: verum

end;

hence lim s2 = a #R (lim s1) by A3, SEQ_2:def 7; :: thesis: verum