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 ;
deffunc H1( Nat) -> set = (((seq_const (lim s1)) /" s1) . \$1) |^ m0;
consider s3 being Real_Sequence such that
A9: for n being Nat holds s3 . n = H1(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 ;
then A12: s3 is convergent by ;
reconsider q = m0 as Rational ;
deffunc H2( Nat) -> set = ((s1 /" (seq_const (lim s1))) . \$1) |^ m0;
consider s4 being Real_Sequence such that
A13: for n being Nat holds s4 . n = H2(n) from SEQ_1:sch 1();
lim ((seq_const (lim s1)) /" s1) = (lim (seq_const (lim s1))) / (lim s1) by
.= 1 by ;
then lim s3 = 1 |^ m0 by ;
then A14: lim s3 = 1 ;
lim (s1 /" (seq_const (lim s1))) = (lim s1) / (lim (seq_const (lim s1))) by
.= 1 by ;
then lim s4 = 1 |^ m0 by ;
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 ;
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 ;
A21: (lim s1) #Q p > 0 by ;
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 ;
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 ;
m1 <= n by NAT_1:11;
then A26: m >= m1 by ;
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 ;
then A29: (s1 /" (seq_const (lim s1))) . m >= 1 by ;
then ((s1 /" (seq_const (lim s1))) . m) #Q p <= ((s1 /" (seq_const (lim s1))) . m) #Q q by ;
then ((s1 /" (seq_const (lim s1))) . m) #Q p <= ((s1 /" (seq_const (lim s1))) . m) |^ m0 by ;
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 ;
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 ;
A33: |.((s4 . m) - 1).| < c / |.((lim s1) #Q p).| by ;
A34: s1 . m > 0 by A5;
((s1 /" (seq_const (lim s1))) . m) |^ m0 >= 1 by ;
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 ;
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 ;
A36: |.((lim s1) #Q p).| <> 0 by ;
|.((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
.= |.((((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
.= |.((lim s1) #Q p).| * |.((((s1 . m) / (lim s1)) #Q p) - 1).| by ;
then |.((s2 . m) - ((lim s1) #Q p)).| < |.((lim s1) #Q p).| * (c / |.((lim s1) #Q p).|) by ;
hence |.((s2 . m) - ((lim s1) #Q p)).| < c by ; :: 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
.= ((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 ;
then A42: ((seq_const (lim s1)) /" s1) . m >= 1 by ;
then (((seq_const (lim s1)) /" s1) . m) #Q p <= (((seq_const (lim s1)) /" s1) . m) #Q q by ;
then (((seq_const (lim s1)) /" s1) . m) #Q p <= (((seq_const (lim s1)) /" s1) . m) |^ m0 by ;
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 ;
then A44: |.((s1 . m) #Q p).| > 0 by ABSVALUE:def 1;
A45: |.((s3 . m) - 1).| < c / d by ;
(((seq_const (lim s1)) /" s1) . m) #Q p >= 1 by ;
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 ;
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 ;
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 ;
|.(s2 . m).| < d by A17;
then |.((s1 . m) #Q p).| < d by A5;
then |.((s1 . m) #Q p).| / d < d / d by ;
then |.((s1 . m) #Q p).| / d < 1 by ;
then A48: c * (|.((s1 . m) #Q p).| / d) < c * 1 by ;
A49: (s1 . m) #Q p <> 0 by ;
|.((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
.= |.((((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
.= |.((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 ;
then |.((s2 . m) - ((lim s1) #Q p)).| < |.((s1 . m) #Q p).| * (c / d) by ;
hence |.((s2 . m) - ((lim s1) #Q p)).| < c by ; :: thesis: verum
end;
end;
end;
hence |.((s2 . m) - ((lim s1) #Q p)).| < c ; :: thesis: verum
end;
hence lim s2 = (lim s1) #Q p by ; :: thesis: verum