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 and
A2: s2 is convergent and
A3: lim s1 > 0 and
A4: p >= 0 and
A5: 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 ;
consider m0 being Element of NAT such that
A6: p < m0 by SEQ_4:3;
A7: lim s = s . 0 by SEQ_4:26
.= lim s1 by FUNCOP_1:7 ;
then A8: s1 /" s is convergent by A1, A3, SEQ_2:23;
deffunc H₁( Element of NAT ) -> Element of REAL = ((s /" s1) . $1) |^ m0;
consider s3 being Real_Sequence such that
A9: for n being Element of NAT holds s3 . n = H₁(n) from SEQ_1:sch 1();
for n being Element of NAT holds s1 . n <> 0 by A5;
then A10: s1 is non-empty by SEQ_1:5;
then A11: s /" s1 is convergent by A1, A3, SEQ_2:23;
then A12: s3 is convergent by A9, Th26;
reconsider q = m0 as Rational ;
deffunc H₂( Element of NAT ) -> Element of REAL = ((s1 /" s) . $1) |^ m0;
consider s4 being Real_Sequence such that
A13: for n being Element of NAT holds s4 . n = H₂(n) from SEQ_1:sch 1();
lim (s /" s1) = (lim s) / (lim s1) by A1, A3, A10, SEQ_2:24
.= 1 by A3, A7, XCMPLX_1:60 ;
then lim s3 = 1 |^ m0 by A11, A9, Th26;
then A14: lim s3 = 1 by NEWTON:10;
lim (s1 /" s) = (lim s1) / (lim s) by A1, A3, A7, SEQ_2:24
.= 1 by A3, A7, XCMPLX_1:60 ;
then lim s4 = 1 |^ m0 by A8, A13, Th26;
then A15: lim s4 = 1 by NEWTON:10;
s2 is bounded by A2, SEQ_2:13;
then consider d being real number such that
A16: d > 0 and
A17: for n being Element of NAT holds abs (s2 . n) < d by SEQ_2:3;
A18: s4 is convergent by A8, A13, Th26;

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

now

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

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

A28: (s1 . m) / (lim s1) = (s1 . m) / (s . m) by FUNCOP_1:7
.= (s1 . m) * ((s . m) ")
.= (s1 . m) * ((s ") . m) by VALUED_1:10
.= (s1 /" s) . m by SEQ_1:8 ;
(s1 . m) * ((lim s1) ") >= (lim s1) * ((lim s1) ") by A3, A27, XREAL_1:64;
then A29: (s1 /" s) . m >= 1 by A3, A28, XCMPLX_0:def 7;
then ((s1 /" s) . m) #Q p <= ((s1 /" s) . m) #Q q by A6, Th74;
then ((s1 /" s) . m) #Q p <= ((s1 /" s) . m) |^ m0 by A29, Th60;
then A30: (((s1 /" s) . m) #Q p) - 1 <= (((s1 /" s) . m) |^ m0) - 1 by XREAL_1:9;
((s1 /" s) . m) #Q p >= 1 by A4, A29, Th71;
then (((s1 /" s) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:9;
then A31: (((s1 /" s) . m) #Q p) - 1 = abs ((((s1 /" s) . m) #Q p) - 1) by ABSVALUE:def 1;
A32: (lim s1) #Q p <> 0 by A3, Th63;
A33: abs ((s4 . m) - 1) < c / (abs ((lim s1) #Q p)) by A23, A25;
A34: s1 . m > 0 by A5;
((s1 /" s) . m) |^ m0 >= 1 by A29, Th19;
then (((s1 /" s) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:9;
then abs ((((s1 /" s) . m) #Q p) - 1) <= abs ((((s1 /" s) . m) |^ m0) - 1) by A30, A31, ABSVALUE:def 1;
then abs ((((s1 /" s) . m) #Q p) - 1) <= abs ((s4 . m) - 1) by A13;
then A35: abs ((((s1 /" s) . m) #Q p) - 1) < c / (abs ((lim s1) #Q p)) by A33, XXREAL_0:2;
A36: abs ((lim s1) #Q p) <> 0 by A21, ABSVALUE:def 1;
abs ((s2 . m) - ((lim s1) #Q p)) = abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1) by A5
.= abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((lim s1) #Q p) / ((lim s1) #Q p))) by A32, 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:65
.= (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 A32, XCMPLX_1:60
.= (abs ((lim s1) #Q p)) * (abs ((((s1 . m) / (lim s1)) #Q p) - 1)) by A3, A34, Th69 ;
then abs ((s2 . m) - ((lim s1) #Q p)) < (abs ((lim s1) #Q p)) * (c / (abs ((lim s1) #Q p))) by A22, A28, A35, XREAL_1:68;
hence abs ((s2 . m) - ((lim s1) #Q p)) < c by A36, XCMPLX_1:87; :: thesis: verum

end;

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

A38: (lim s1) / (s1 . m) = (s . m) / (s1 . m) by FUNCOP_1:7
.= (s . m) * ((s1 . m) ")
.= (s . m) * ((s1 ") . m) by VALUED_1:10
.= (s /" s1) . m by SEQ_1:8 ;
A39: s1 . m <> 0 by A5;
A40: s1 . m > 0 by A5;
then (s1 . m) * ((s1 . m) ") <= (lim s1) * ((s1 . m) ") by A37, XREAL_1:64;
then A41: (s /" s1) . m >= 1 by A39, A38, XCMPLX_0:def 7;
then ((s /" s1) . m) #Q p <= ((s /" s1) . m) #Q q by A6, Th74;
then ((s /" s1) . m) #Q p <= ((s /" s1) . m) |^ m0 by A41, Th60;
then A42: (((s /" s1) . m) #Q p) - 1 <= (((s /" s1) . m) |^ m0) - 1 by XREAL_1:9;
(s1 . m) #Q p > 0 by A5, Th63;
then A43: abs ((s1 . m) #Q p) > 0 by ABSVALUE:def 1;
A44: abs ((s3 . m) - 1) < c / d by A20, A26;
((s /" s1) . m) #Q p >= 1 by A4, A41, Th71;
then (((s /" s1) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:9;
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 A41, Th19;
then (((s /" s1) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:9;
then abs ((((s /" s1) . m) #Q p) - 1) <= abs ((((s /" s1) . m) |^ m0) - 1) by A42, A45, ABSVALUE:def 1;
then abs ((((s /" s1) . m) #Q p) - 1) <= abs ((s3 . m) - 1) by A9;
then A46: abs ((((s /" s1) . m) #Q p) - 1) < c / d by A44, XXREAL_0:2;
abs (s2 . m) < d by A17;
then abs ((s1 . m) #Q p) < d by A5;
then (abs ((s1 . m) #Q p)) / d < d / d by A16, XREAL_1:74;
then (abs ((s1 . m) #Q p)) / d < 1 by A16, XCMPLX_1:60;
then A47: c * ((abs ((s1 . m) #Q p)) / d) < c * 1 by A19, XREAL_1:68;
A48: (s1 . m) #Q p <> 0 by A5, Th63;
abs ((s2 . m) - ((lim s1) #Q p)) = abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1) by A5
.= abs ((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((s1 . m) #Q p) / ((s1 . m) #Q p))) by A48, 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:65
.= (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 A48, XCMPLX_1:60
.= (abs ((s1 . m) #Q p)) * (abs (- (1 - (((lim s1) #Q p) / ((s1 . m) #Q p))))) by COMPLEX1:52
.= (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 A3, A40, Th69 ;
then abs ((s2 . m) - ((lim s1) #Q p)) < (abs ((s1 . m) #Q p)) * (c / d) by A43, A38, A46, XREAL_1:68;
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 A2, SEQ_2:def 7; :: thesis: verum