let p be Rational; :: thesis: for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) holds
lim s2 = (lim s1) #Q p
let s1, s2 be Real_Sequence; :: thesis: ( s1 is convergent & s2 is convergent & lim s1 > 0 & p >= 0 & ( for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ) implies lim s2 = (lim s1) #Q p )
assume that
A1: ( s1 is convergent & s2 is convergent ) and
A2: ( lim s1 > 0 & p >= 0 ) and
A3: for n being Element of NAT holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ; :: thesis: lim s2 = (lim s1) #Q p
reconsider s = NAT --> (lim s1) as Real_Sequence ;
A5: lim s = s . 0 by SEQ_4:41
.= lim s1 by FUNCOP_1:13 ;
for n being Element of NAT holds s1 . n <> 0 by A3;
then A6: s1 is non-zero by SEQ_1:7;
A8: s1 /" s is convergent by A1, A2, A5, SEQ_2:37;
A9: lim (s1 /" s) = (lim s1) / (lim s) by A1, A2, A5, SEQ_2:38
.= 1 by A2, A5, XCMPLX_1:60 ;
A10: s /" s1 is convergent by A1, A2, A6, SEQ_2:37;
A11: lim (s /" s1) = (lim s) / (lim s1) by A1, A2, A6, SEQ_2:38
.= 1 by A2, A5, XCMPLX_1:60 ;
consider m0 being Element of NAT such that
A12: p < m0 by SEQ_4:10;
reconsider q = m0 as Rational ;
deffunc H₁( Element of NAT ) -> Element of REAL = ((s /" s1) . $1) |^ m0;
consider s3 being Real_Sequence such that
A13: for n being Element of NAT holds s3 . n = H₁(n) from SEQ_1:sch 1();
deffunc H₂( Element of NAT ) -> Element of REAL = ((s1 /" s) . $1) |^ m0;
consider s4 being Real_Sequence such that
A14: for n being Element of NAT holds s4 . n = H₂(n) from SEQ_1:sch 1();
( s3 is convergent & lim s3 = 1 |^ m0 ) by A10, A11, A13, Th26;
then A15: ( s3 is convergent & lim s3 = 1 ) by NEWTON:15;
( s4 is convergent & lim s4 = 1 |^ m0 ) by A8, A9, A14, Th26;
then A16: ( s4 is convergent & lim s4 = 1 ) by NEWTON:15;
s2 is bounded by A1, SEQ_2:27;
then consider d being real number such that
A17: ( d > 0 & ( for n being Element of NAT holds abs (s2 . n) < d ) ) by SEQ_2:15;

now

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) - ((lim s1) #Q p)) < c )
assume A18: c > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((s2 . m) - ((lim s1) #Q p)) < c
then c / d > 0 by A17, XREAL_1:141;
then consider m1 being Element of NAT such that
A19: for m being Element of NAT st m >= m1 holds
abs ((s3 . m) - 1) < c / d by A15, SEQ_2:def 7;
A20: (lim s1) #Q p > 0 by A2, Th63;
then A21: abs ((lim s1) #Q p) > 0 by ABSVALUE:def 1;
then c / (abs ((lim s1) #Q p)) > 0 by A18, XREAL_1:141;
then consider m2 being Element of NAT such that
A22: for m being Element of NAT st m >= m2 holds
abs ((s4 . m) - 1) < c / (abs ((lim s1) #Q p)) by A16, SEQ_2:def 7;
take n = m1 + m2; :: thesis: for m being Element of NAT st m >= n holds
abs ((s2 . m) - ((lim s1) #Q p)) < c
let m be Element of NAT ; :: thesis: ( m >= n implies abs ((s2 . m) - ((lim s1) #Q p)) < c )
assume A23: m >= n ; :: thesis: abs ((s2 . m) - ((lim s1) #Q p)) < c
m1 <= n by NAT_1:11;
then A24: m >= m1 by A23, XXREAL_0:2;
m2 <= n by NAT_1:11;
then A25: m >= m2 by A23, XXREAL_0:2;

now

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

suppose A26: s1 . m >= lim s1 ; :: thesis: abs ((s2 . m) - ((lim s1) #Q p)) < c

A27: (lim s1) #Q p <> 0 by A2, Th63;
A28: abs ((lim s1) #Q p) <> 0 by A20, ABSVALUE:def 1;
A29: s1 . m > 0 by A3;
A30: abs ((s2 . m) - ((lim s1) #Q p)) = abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1) by A3
.= abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((lim s1) #Q p) / ((lim s1) #Q p))) by A27, XCMPLX_1:60
.= abs ((((lim s1) #Q p) * (((s1 . m) #Q p) - ((lim s1) #Q p))) / ((lim s1) #Q p))
.= abs (((lim s1) #Q p) * ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((lim s1) #Q p)))
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((lim s1) #Q p))) by COMPLEX1:151
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) #Q p) / ((lim s1) #Q p)) - (((lim s1) #Q p) / ((lim s1) #Q p))))
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) #Q p) / ((lim s1) #Q p)) - 1)) by A27, XCMPLX_1:60
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) / (lim s1)) #Q p) - 1)) by A2, A29, Th69 ;
A31: (s1 . m) / (lim s1) = (s1 . m) / (s . m) by FUNCOP_1:13
.= (s1 . m) * ((s . m) " )
.= (s1 . m) * ((s " ) . m) by VALUED_1:10
.= (s1 /" s) . m by SEQ_1:12 ;
(lim s1) " >= 0 by A2;
then (s1 . m) * ((lim s1) " ) >= (lim s1) * ((lim s1) " ) by A26, XREAL_1:66;
then (s1 . m) * ((lim s1) " ) >= 1 by A2, XCMPLX_0:def 7;
then A32: (s1 /" s) . m >= 1 by A31;
then ((s1 /" s) . m) #Q p <= ((s1 /" s) . m) #Q q by A12, Th74;
then ((s1 /" s) . m) #Q p <= ((s1 /" s) . m) |^ m0 by A32, Th60;
then A33: (((s1 /" s) . m) #Q p) - 1 <= (((s1 /" s) . m) |^ m0) - 1 by XREAL_1:11;
((s1 /" s) . m) #Q p >= 1 by A2, A32, Th71;
then (((s1 /" s) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:11;
then A34: (((s1 /" s) . m) #Q p) - 1 = abs ((((s1 /" s) . m) #Q p) - 1) by ABSVALUE:def 1;
((s1 /" s) . m) |^ m0 >= 1 by A32, Th19;
then (((s1 /" s) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:11;
then abs ((((s1 /" s) . m) #Q p) - 1) <= abs ((((s1 /" s) . m) |^ m0) - 1) by A33, A34, ABSVALUE:def 1;
then A35: abs ((((s1 /" s) . m) #Q p) - 1) <= abs ((s4 . m) - 1) by A14;
abs ((s4 . m) - 1) < c / (abs ((lim s1) #Q p)) by A22, A25;
then abs ((((s1 /" s) . m) #Q p) - 1) < c / (abs ((lim s1) #Q p)) by A35, XXREAL_0:2;
then abs ((s2 . m) - ((lim s1) #Q p)) < (abs ((lim s1) #Q p)) * (c / (abs ((lim s1) #Q p))) by A21, A30, A31, XREAL_1:70;
hence abs ((s2 . m) - ((lim s1) #Q p)) < c by A28, XCMPLX_1:88; :: thesis: verum

end;

suppose A36: s1 . m <= lim s1 ; :: thesis: abs ((s2 . m) - ((lim s1) #Q p)) < c

A37: s1 . m > 0 by A3;
then (s1 . m) #Q p > 0 by Th63;
then A38: abs ((s1 . m) #Q p) > 0 by ABSVALUE:def 1;
A39: (s1 . m) #Q p <> 0 by A37, Th63;
A40: s1 . m <> 0 by A3;
A41: abs ((s2 . m) - ((lim s1) #Q p)) = abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1) by A3
.= abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((s1 . m) #Q p) / ((s1 . m) #Q p))) by A39, XCMPLX_1:60
.= abs ((((s1 . m) #Q p) * (((s1 . m) #Q p) - ((lim s1) #Q p))) / ((s1 . m) #Q p))
.= abs (((s1 . m) #Q p) * ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((s1 . m) #Q p)))
.= (abs ((s1 . m) #Q p)) * (abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((s1 . m) #Q p))) by COMPLEX1:151
.= (abs ((s1 . m) #Q p)) * (abs ((((s1 . m) #Q p) / ((s1 . m) #Q p)) - (((lim s1) #Q p) / ((s1 . m) #Q p))))
.= (abs ((s1 . m) #Q p)) * (abs (1 - (((lim s1) #Q p) / ((s1 . m) #Q p)))) by A39, XCMPLX_1:60
.= (abs ((s1 . m) #Q p)) * (abs (- (1 - (((lim s1) #Q p) / ((s1 . m) #Q p))))) by COMPLEX1:138
.= (abs ((s1 . m) #Q p)) * (abs ((((lim s1) #Q p) / ((s1 . m) #Q p)) - 1))
.= (abs ((s1 . m) #Q p)) * (abs ((((lim s1) / (s1 . m)) #Q p) - 1)) by A2, A37, Th69 ;
A42: (lim s1) / (s1 . m) = (s . m) / (s1 . m) by FUNCOP_1:13
.= (s . m) * ((s1 . m) " )
.= (s . m) * ((s1 " ) . m) by VALUED_1:10
.= (s /" s1) . m by SEQ_1:12 ;
(s1 . m) " >= 0 by A37;
then (s1 . m) * ((s1 . m) " ) <= (lim s1) * ((s1 . m) " ) by A36, XREAL_1:66;
then (lim s1) * ((s1 . m) " ) >= 1 by A40, XCMPLX_0:def 7;
then A43: (s /" s1) . m >= 1 by A42;
then ((s /" s1) . m) #Q p <= ((s /" s1) . m) #Q q by A12, Th74;
then ((s /" s1) . m) #Q p <= ((s /" s1) . m) |^ m0 by A43, Th60;
then A44: (((s /" s1) . m) #Q p) - 1 <= (((s /" s1) . m) |^ m0) - 1 by XREAL_1:11;
((s /" s1) . m) #Q p >= 1 by A2, A43, Th71;
then (((s /" s1) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:11;
then A45: (((s /" s1) . m) #Q p) - 1 = abs ((((s /" s1) . m) #Q p) - 1) by ABSVALUE:def 1;
((s /" s1) . m) |^ m0 >= 1 by A43, Th19;
then (((s /" s1) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:11;
then abs ((((s /" s1) . m) #Q p) - 1) <= abs ((((s /" s1) . m) |^ m0) - 1) by A44, A45, ABSVALUE:def 1;
then A46: abs ((((s /" s1) . m) #Q p) - 1) <= abs ((s3 . m) - 1) by A13;
abs ((s3 . m) - 1) < c / d by A19, A24;
then abs ((((s /" s1) . m) #Q p) - 1) < c / d by A46, XXREAL_0:2;
then abs ((s2 . m) - ((lim s1) #Q p)) < (abs ((s1 . m) #Q p)) * (c / d) by A38, A41, A42, XREAL_1:70;
then abs ((s2 . m) - ((lim s1) #Q p)) < (c * (abs ((s1 . m) #Q p))) / d ;
then A47: abs ((s2 . m) - ((lim s1) #Q p)) < c * ((abs ((s1 . m) #Q p)) / d) ;
abs (s2 . m) < d by A17;
then abs ((s1 . m) #Q p) < d by A3;
then (abs ((s1 . m) #Q p)) / d < d / d by A17, XREAL_1:76;
then (abs ((s1 . m) #Q p)) / d < 1 by A17, XCMPLX_1:60;
then c * ((abs ((s1 . m) #Q p)) / d) < c * 1 by A18, XREAL_1:70;
hence abs ((s2 . m) - ((lim s1) #Q p)) < c by A47, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence abs ((s2 . m) - ((lim s1) #Q p)) < c ; :: thesis: verum

end;

hence lim s2 = (lim s1) #Q p by A1, SEQ_2:def 7; :: thesis: verum