let a be real number ; :: thesis: for s1, s2 being Real_Sequence st a >= 1 & s1 is convergent & s2 is convergent & ( for n being Element of 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 Element of 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 Element of NAT holds s2 . n = a #R (s1 . n) ; :: thesis: lim s2 = a #R (lim s1)
set d = (abs (lim s1)) + 1;
A5: abs (lim s1) < (abs (lim s1)) + 1 by XREAL_1:29;

now

lim s1 <= abs (lim s1) by ABSVALUE:4;
then lim s1 <= (abs (lim s1)) + 1 by A5, XXREAL_0:2;
then A6: a #R (lim s1) <= a #R ((abs (lim s1)) + 1) by A1, Th96;
a #R (lim s1) > 0 by A1, Th95;
then A7: abs (a #R (lim s1)) <= a #R ((abs (lim s1)) + 1) by A6, ABSVALUE:def 1;
A8: a #R ((abs (lim s1)) + 1) >= 0 by A1, Th95;
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 ((s2 . m) - (a #R (lim s1))) < c )
assume A9: c > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((s2 . m) - (a #R (lim s1))) < c
consider m1 being Element of NAT such that
A10: ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / c < m1 by SEQ_4:3;
m1 + 1 >= m1 by XREAL_1:29;
then ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / c < m1 + 1 by A10, XXREAL_0:2;
then (((a #R ((abs (lim s1)) + 1)) * (a - 1)) / c) * c < c * (m1 + 1) by A9, XREAL_1:68;
then (a #R ((abs (lim s1)) + 1)) * (a - 1) < c * (m1 + 1) by A9, XCMPLX_1:87;
then ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:74;
then ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A11: ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:87;
reconsider m3 = (m1 + 1) " as Rational ;
A12: abs (a #R (lim s1)) >= 0 by COMPLEX1:46;
consider n being Element of NAT such that
A13: for m being Element of NAT st n <= m holds
abs ((s1 . m) - (lim s1)) < (m1 + 1) " by A2, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st m >= n holds
abs ((s2 . m) - (a #R (lim s1))) < c
let m be Element of NAT ; :: thesis: ( m >= n implies abs ((s2 . m) - (a #R (lim s1))) < c )
assume m >= n ; :: thesis: abs ((s2 . m) - (a #R (lim s1))) < c
then A14: abs ((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, Th40;
then A16: (a #R ((abs (lim s1)) + 1)) * (((m1 + 1) -Root a) - 1) <= (a #R ((abs (lim s1)) + 1)) * ((a - 1) / (m1 + 1)) by A8, XREAL_1:64;
(s1 . m) - (lim s1) <= abs ((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, Th96;
then a #R ((s1 . m) - (lim s1)) <= a #Q m3 by A1, Th88;
then a #R ((s1 . m) - (lim s1)) <= (m1 + 1) -Root a by A15, Th61;
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, Th95;
A19: a #R ((s1 . m) - (lim s1)) > 0 by A1, Th95;

A20: now

per cases ( (s1 . m) - (lim s1) >= 0 or (s1 . m) - (lim s1) < 0 ) ;

suppose (s1 . m) - (lim s1) >= 0 ; :: thesis: abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1

then a #R ((s1 . m) - (lim s1)) >= 1 by A1, Th99;
then (a #R ((s1 . m) - (lim s1))) - 1 >= 0 by XREAL_1:48;
hence abs ((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: abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1

A22: - ((s1 . m) - (lim s1)) <= abs (- ((s1 . m) - (lim s1))) by ABSVALUE:4;
abs ((s1 . m) - (lim s1)) = abs (- ((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, Th96;
then a #R (- ((s1 . m) - (lim s1))) <= a #Q m3 by A1, Th88;
then a #R (- ((s1 . m) - (lim s1))) <= (m1 + 1) -Root a by A15, Th61;
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, Th99;
then (a #R (- ((s1 . m) - (lim s1)))) - 1 >= 0 by XREAL_1:48;
then A24: abs ((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, Th101;
then A25: abs (a #R ((s1 . m) - (lim s1))) <= 1 by A19, ABSVALUE:def 1;
abs ((a #R (- ((s1 . m) - (lim s1)))) - 1) >= 0 by COMPLEX1:46;
then A26: (abs (a #R ((s1 . m) - (lim s1)))) * (abs ((a #R (- ((s1 . m) - (lim s1)))) - 1)) <= 1 * (abs ((a #R (- ((s1 . m) - (lim s1)))) - 1)) by A25, XREAL_1:64;
abs ((a #R ((s1 . m) - (lim s1))) - 1) = abs (((a #R ((s1 . m) - (lim s1))) - 1) * 1)
.= abs (((a #R ((s1 . m) - (lim s1))) - 1) * ((a #R ((s1 . m) - (lim s1))) / (a #R ((s1 . m) - (lim s1))))) by A18, XCMPLX_1:60
.= abs (((a #R ((s1 . m) - (lim s1))) * ((a #R ((s1 . m) - (lim s1))) - 1)) / (a #R ((s1 . m) - (lim s1))))
.= abs ((a #R ((s1 . m) - (lim s1))) * (((a #R ((s1 . m) - (lim s1))) - 1) / (a #R ((s1 . m) - (lim s1)))))
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (((a #R ((s1 . m) - (lim s1))) - 1) / (a #R ((s1 . m) - (lim s1))))) by COMPLEX1:65
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (((a #R ((s1 . m) - (lim s1))) / (a #R ((s1 . m) - (lim s1)))) - (1 / (a #R ((s1 . m) - (lim s1))))))
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (1 - (1 / (a #R ((s1 . m) - (lim s1)))))) by A18, XCMPLX_1:60
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (1 - (a #R (- ((s1 . m) - (lim s1)))))) by A1, Th90
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs (- (1 - (a #R (- ((s1 . m) - (lim s1))))))) by COMPLEX1:52
.= (abs (a #R ((s1 . m) - (lim s1)))) * (abs ((a #R (- ((s1 . m) - (lim s1)))) - 1)) ;
hence abs ((a #R ((s1 . m) - (lim s1))) - 1) <= ((m1 + 1) -Root a) - 1 by A24, A26, XXREAL_0:2; :: thesis: verum

end;

end;

end;

abs ((a #R ((s1 . m) - (lim s1))) - 1) >= 0 by COMPLEX1:46;
then A27: (abs (a #R (lim s1))) * (abs ((a #R ((s1 . m) - (lim s1))) - 1)) <= (a #R ((abs (lim s1)) + 1)) * (((m1 + 1) -Root a) - 1) by A20, A12, A7, XREAL_1:66;
abs ((a #R (s1 . m)) - (a #R (lim s1))) = abs (((a #R (s1 . m)) - (a #R (lim s1))) * 1)
.= abs (((a #R (s1 . m)) - (a #R (lim s1))) * ((a #R (lim s1)) / (a #R (lim s1)))) by A1, Lm9, XCMPLX_1:60
.= abs (((a #R (lim s1)) * ((a #R (s1 . m)) - (a #R (lim s1)))) / (a #R (lim s1)))
.= abs ((a #R (lim s1)) * (((a #R (s1 . m)) - (a #R (lim s1))) / (a #R (lim s1))))
.= (abs (a #R (lim s1))) * (abs (((a #R (s1 . m)) - (a #R (lim s1))) / (a #R (lim s1)))) by COMPLEX1:65
.= (abs (a #R (lim s1))) * (abs (((a #R (s1 . m)) / (a #R (lim s1))) - ((a #R (lim s1)) / (a #R (lim s1)))))
.= (abs (a #R (lim s1))) * (abs (((a #R (s1 . m)) / (a #R (lim s1))) - 1)) by A1, Lm9, XCMPLX_1:60
.= (abs (a #R (lim s1))) * (abs ((a #R ((s1 . m) - (lim s1))) - 1)) by A1, Th91 ;
then abs ((a #R (s1 . m)) - (a #R (lim s1))) <= ((a #R ((abs (lim s1)) + 1)) * (a - 1)) / (m1 + 1) by A27, A16, XXREAL_0:2;
then abs ((a #R (s1 . m)) - (a #R (lim s1))) < c by A11, XXREAL_0:2;
hence abs ((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