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 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 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 Nat holds
( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ; :: thesis: lim s2 = (lim s1) #Q p
reconsider ls = lim s1 as Element of REAL by XREAL_0:def 1;
set s = seq_const (lim s1);
consider m0 being Nat such that
A6: p < m0 by SEQ_4:3;
A7: lim (seq_const (lim s1)) = (seq_const (lim s1)) . 0 by SEQ_4:26
.= lim s1 by FUNCOP_1:7 ;
then A8: s1 /" (seq_const (lim s1)) is convergent by A1, A3, SEQ_2:23;
deffunc H₁( Nat) -> set = (((seq_const (lim s1)) /" s1) . $1) |^ m0;
consider s3 being Real_Sequence such that
A9: for n being Nat holds s3 . n = H₁(n) from SEQ_1:sch 1();
for n being Nat holds s1 . n <> 0 by A5;
then A10: s1 is non-zero by SEQ_1:5;
then A11: (seq_const (lim s1)) /" s1 is convergent by A1, A3, SEQ_2:23;
then A12: s3 is convergent by A9, Th18;
reconsider q = m0 as Rational ;
deffunc H₂( Nat) -> set = ((s1 /" (seq_const (lim s1))) . $1) |^ m0;
consider s4 being Real_Sequence such that
A13: for n being Nat holds s4 . n = H₂(n) from SEQ_1:sch 1();
lim ((seq_const (lim s1)) /" s1) = (lim (seq_const (lim s1))) / (lim s1) by A1, A3, A10, SEQ_2:24
.= 1 by A3, A7, XCMPLX_1:60 ;
then lim s3 = 1 |^ m0 by A11, A9, Th18;
then A14: lim s3 = 1 ;
lim (s1 /" (seq_const (lim s1))) = (lim s1) / (lim (seq_const (lim s1))) by A1, A3, A7, SEQ_2:24
.= 1 by A3, A7, XCMPLX_1:60 ;
then lim s4 = 1 |^ m0 by A8, A13, Th18;
then A15: lim s4 = 1 ;
s2 is bounded by A2;
then consider d being Real such that
A16: d > 0 and
A17: for n being Nat holds |.(s2 . n).| < d by SEQ_2:3;
A18: s4 is convergent by A8, A13, Th18;

now :: thesis: for c being Real st c > 0 holds
ex n being set st
for m being Nat st m >= n holds
|.((s2 . m) - ((lim s1) #Q p)).| < c

let c be Real; :: thesis: ( c > 0 implies ex n being set st
for m being Nat st m >= n holds
|.((s2 . m) - ((lim s1) #Q p)).| < c )
assume A19: c > 0 ; :: thesis: ex n being set st
for m being Nat st m >= n holds
|.((s2 . m) - ((lim s1) #Q p)).| < c
then c / d > 0 by A16;
then consider m1 being Nat such that
A20: for m being Nat st m >= m1 holds
|.((s3 . m) - 1).| < c / d by A12, A14, SEQ_2:def 7;
A21: (lim s1) #Q p > 0 by A3, Th52;
then A22: |.((lim s1) #Q p).| > 0 by ABSVALUE:def 1;
then c / |.((lim s1) #Q p).| > 0 by A19;
then consider m2 being Nat such that
A23: for m being Nat st m >= m2 holds
|.((s4 . m) - 1).| < c / |.((lim s1) #Q p).| by A18, A15, SEQ_2:def 7;
take n = m1 + m2; :: thesis: for m being Nat st m >= n holds
|.((s2 . m) - ((lim s1) #Q p)).| < c
let m be Nat; :: thesis: ( m >= n implies |.((s2 . m) - ((lim s1) #Q p)).| < c )
assume A24: m >= n ; :: thesis: |.((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 :: thesis: |.((s2 . m) - ((lim s1) #Q p)).| < c

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

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

m in NAT by ORDINAL1:def 12;
then A28: (s1 . m) / (lim s1) = (s1 . m) / ((seq_const (lim s1)) . m) by FUNCOP_1:7
.= (s1 . m) * (((seq_const (lim s1)) . m) ")
.= (s1 . m) * (((seq_const (lim s1)) ") . m) by VALUED_1:10
.= (s1 /" (seq_const (lim s1))) . m by SEQ_1:8 ;
(s1 . m) * ((lim s1) ") >= (lim s1) * ((lim s1) ") by A3, A27, XREAL_1:64;
then A29: (s1 /" (seq_const (lim s1))) . m >= 1 by A3, A28, XCMPLX_0:def 7;
then ((s1 /" (seq_const (lim s1))) . m) #Q p <= ((s1 /" (seq_const (lim s1))) . m) #Q q by A6, Th63;
then ((s1 /" (seq_const (lim s1))) . m) #Q p <= ((s1 /" (seq_const (lim s1))) . m) |^ m0 by A29, Th49;
then A30: (((s1 /" (seq_const (lim s1))) . m) #Q p) - 1 <= (((s1 /" (seq_const (lim s1))) . m) |^ m0) - 1 by XREAL_1:9;
((s1 /" (seq_const (lim s1))) . m) #Q p >= 1 by A4, A29, Th60;
then (((s1 /" (seq_const (lim s1))) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:9;
then A31: (((s1 /" (seq_const (lim s1))) . m) #Q p) - 1 = |.((((s1 /" (seq_const (lim s1))) . m) #Q p) - 1).| by ABSVALUE:def 1;
A32: (lim s1) #Q p <> 0 by A3, Th52;
A33: |.((s4 . m) - 1).| < c / |.((lim s1) #Q p).| by A23, A25;
A34: s1 . m > 0 by A5;
((s1 /" (seq_const (lim s1))) . m) |^ m0 >= 1 by A29, Th11;
then (((s1 /" (seq_const (lim s1))) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:9;
then |.((((s1 /" (seq_const (lim s1))) . m) #Q p) - 1).| <= |.((((s1 /" (seq_const (lim s1))) . m) |^ m0) - 1).| by A30, A31, ABSVALUE:def 1;
then |.((((s1 /" (seq_const (lim s1))) . m) #Q p) - 1).| <= |.((s4 . m) - 1).| by A13;
then A35: |.((((s1 /" (seq_const (lim s1))) . m) #Q p) - 1).| < c / |.((lim s1) #Q p).| by A33, XXREAL_0:2;
A36: |.((lim s1) #Q p).| <> 0 by A21, ABSVALUE:def 1;
|.((s2 . m) - ((lim s1) #Q p)).| = |.((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1).| by A5
.= |.((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((lim s1) #Q p) / ((lim s1) #Q p))).| by A32, XCMPLX_1:60
.= |.((((lim s1) #Q p) * (((s1 . m) #Q p) - ((lim s1) #Q p))) / ((lim s1) #Q p)).|
.= |.(((lim s1) #Q p) * ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((lim s1) #Q p))).|
.= |.((lim s1) #Q p).| * |.((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((lim s1) #Q p)).| by COMPLEX1:65
.= |.((lim s1) #Q p).| * |.((((s1 . m) #Q p) / ((lim s1) #Q p)) - (((lim s1) #Q p) / ((lim s1) #Q p))).|
.= |.((lim s1) #Q p).| * |.((((s1 . m) #Q p) / ((lim s1) #Q p)) - 1).| by A32, XCMPLX_1:60
.= |.((lim s1) #Q p).| * |.((((s1 . m) / (lim s1)) #Q p) - 1).| by A3, A34, Th58 ;
then |.((s2 . m) - ((lim s1) #Q p)).| < |.((lim s1) #Q p).| * (c / |.((lim s1) #Q p).|) by A22, A28, A35, XREAL_1:68;
hence |.((s2 . m) - ((lim s1) #Q p)).| < c by A36, XCMPLX_1:87; :: thesis: verum

end;

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

A38: m in NAT by ORDINAL1:def 12;
A39: (lim s1) / (s1 . m) = ((seq_const (lim s1)) . m) / (s1 . m) by FUNCOP_1:7, A38
.= ((seq_const (lim s1)) . m) * ((s1 . m) ")
.= ((seq_const (lim s1)) . m) * ((s1 ") . m) by VALUED_1:10
.= ((seq_const (lim s1)) /" s1) . m by SEQ_1:8 ;
A40: s1 . m <> 0 by A5;
A41: s1 . m > 0 by A5;
then (s1 . m) * ((s1 . m) ") <= (lim s1) * ((s1 . m) ") by A37, XREAL_1:64;
then A42: ((seq_const (lim s1)) /" s1) . m >= 1 by A40, A39, XCMPLX_0:def 7;
then (((seq_const (lim s1)) /" s1) . m) #Q p <= (((seq_const (lim s1)) /" s1) . m) #Q q by A6, Th63;
then (((seq_const (lim s1)) /" s1) . m) #Q p <= (((seq_const (lim s1)) /" s1) . m) |^ m0 by A42, Th49;
then A43: ((((seq_const (lim s1)) /" s1) . m) #Q p) - 1 <= ((((seq_const (lim s1)) /" s1) . m) |^ m0) - 1 by XREAL_1:9;
(s1 . m) #Q p > 0 by A5, Th52;
then A44: |.((s1 . m) #Q p).| > 0 by ABSVALUE:def 1;
A45: |.((s3 . m) - 1).| < c / d by A20, A26;
(((seq_const (lim s1)) /" s1) . m) #Q p >= 1 by A4, A42, Th60;
then ((((seq_const (lim s1)) /" s1) . m) #Q p) - 1 >= 1 - 1 by XREAL_1:9;
then A46: ((((seq_const (lim s1)) /" s1) . m) #Q p) - 1 = |.(((((seq_const (lim s1)) /" s1) . m) #Q p) - 1).| by ABSVALUE:def 1;
(((seq_const (lim s1)) /" s1) . m) |^ m0 >= 1 by A42, Th11;
then ((((seq_const (lim s1)) /" s1) . m) |^ m0) - 1 >= 1 - 1 by XREAL_1:9;
then |.(((((seq_const (lim s1)) /" s1) . m) #Q p) - 1).| <= |.(((((seq_const (lim s1)) /" s1) . m) |^ m0) - 1).| by A43, A46, ABSVALUE:def 1;
then |.(((((seq_const (lim s1)) /" s1) . m) #Q p) - 1).| <= |.((s3 . m) - 1).| by A9;
then A47: |.(((((seq_const (lim s1)) /" s1) . m) #Q p) - 1).| < c / d by A45, XXREAL_0:2;
|.(s2 . m).| < d by A17;
then |.((s1 . m) #Q p).| < d by A5;
then |.((s1 . m) #Q p).| / d < d / d by A16, XREAL_1:74;
then |.((s1 . m) #Q p).| / d < 1 by A16, XCMPLX_1:60;
then A48: c * (|.((s1 . m) #Q p).| / d) < c * 1 by A19, XREAL_1:68;
A49: (s1 . m) #Q p <> 0 by A5, Th52;
|.((s2 . m) - ((lim s1) #Q p)).| = |.((((s1 . m) #Q p) - ((lim s1) #Q p)) * 1).| by A5
.= |.((((s1 . m) #Q p) - ((lim s1) #Q p)) * (((s1 . m) #Q p) / ((s1 . m) #Q p))).| by A49, XCMPLX_1:60
.= |.((((s1 . m) #Q p) * (((s1 . m) #Q p) - ((lim s1) #Q p))) / ((s1 . m) #Q p)).|
.= |.(((s1 . m) #Q p) * ((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((s1 . m) #Q p))).|
.= |.((s1 . m) #Q p).| * |.((((s1 . m) #Q p) - ((lim s1) #Q p)) / ((s1 . m) #Q p)).| by COMPLEX1:65
.= |.((s1 . m) #Q p).| * |.((((s1 . m) #Q p) / ((s1 . m) #Q p)) - (((lim s1) #Q p) / ((s1 . m) #Q p))).|
.= |.((s1 . m) #Q p).| * |.(1 - (((lim s1) #Q p) / ((s1 . m) #Q p))).| by A49, XCMPLX_1:60
.= |.((s1 . m) #Q p).| * |.(- (1 - (((lim s1) #Q p) / ((s1 . m) #Q p)))).| by COMPLEX1:52
.= |.((s1 . m) #Q p).| * |.((((lim s1) #Q p) / ((s1 . m) #Q p)) - 1).|
.= |.((s1 . m) #Q p).| * |.((((lim s1) / (s1 . m)) #Q p) - 1).| by A3, A41, Th58 ;
then |.((s2 . m) - ((lim s1) #Q p)).| < |.((s1 . m) #Q p).| * (c / d) by A44, A39, A47, XREAL_1:68;
hence |.((s2 . m) - ((lim s1) #Q p)).| < c by A48, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence |.((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