let p be Rational; :: thesis: for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 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 & ( 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: for n being Nat holds

( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ; :: thesis: lim s2 = (lim s1) #Q p

( 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 & ( 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: for n being Nat holds

( s1 . n > 0 & s2 . n = (s1 . n) #Q p ) ; :: thesis: lim s2 = (lim s1) #Q p

per cases
( p >= 0 or p <= 0 )
;

end;

suppose A5:
p <= 0
; :: thesis: lim s2 = (lim s1) #Q p

s1 is bounded
by A1;

then consider d being Real such that

A6: d > 0 and

A7: for n being Nat holds |.(s1 . n).| < d by SEQ_2:3;

reconsider d = d as Real ;

A8: d #Q p > 0 by A6, Th52;

then A17: lim (s2 ") = (lim s2) " by A2, A9, SEQ_2:22;

deffunc H_{1}( Nat) -> object = (s2 . $1) " ;

consider s being Real_Sequence such that

A18: for n being Nat holds s . n = H_{1}(n)
from SEQ_1:sch 1();

A21: dom s = NAT by FUNCT_2:def 1;

for n being object st n in dom s holds

s . n = (s2 . n) " by A18;

then A22: s = s2 " by A21, A20, VALUED_1:def 7;

s2 " is convergent by A2, A16, A9, SEQ_2:21;

then (lim s2) " = (lim s1) #Q (- p) by A1, A3, A5, A17, A22, A19, Lm10;

then 1 / (lim s2) = 1 / ((lim s1) #Q p) by A3, Th54;

hence lim s2 = (lim s1) #Q p by XCMPLX_1:59; :: thesis: verum

end;then consider d being Real such that

A6: d > 0 and

A7: for n being Nat holds |.(s1 . n).| < d by SEQ_2:3;

reconsider d = d as Real ;

A8: d #Q p > 0 by A6, Th52;

A9: now :: thesis: not lim s2 = 0

assume
lim s2 = 0
; :: thesis: contradiction

then consider n being Nat such that

A10: for m being Nat st m >= n holds

|.((s2 . m) - 0).| < d #Q p by A2, A8, SEQ_2:def 7;

end;then consider n being Nat such that

A10: for m being Nat st m >= n holds

|.((s2 . m) - 0).| < d #Q p by A2, A8, SEQ_2:def 7;

now :: thesis: for m being Nat holds not m >= n

hence
contradiction
; :: thesis: verumlet m be Nat; :: thesis: not m >= n

A11: s1 . m > 0 by A4;

A12: s1 . m <> 0 by A4;

A13: (s1 . m) #Q p > 0 by A4, Th52;

|.(s1 . m).| < d by A7;

then s1 . m < d by A11, ABSVALUE:def 1;

then (s1 . m) / (s1 . m) < d / (s1 . m) by A11, XREAL_1:74;

then 1 <= d / (s1 . m) by A12, XCMPLX_1:60;

then (d / (s1 . m)) #Q p <= 1 by A5, Th61;

then (d #Q p) / ((s1 . m) #Q p) <= 1 by A6, A11, Th58;

then A14: ((d #Q p) / ((s1 . m) #Q p)) * ((s1 . m) #Q p) <= 1 * ((s1 . m) #Q p) by A13, XREAL_1:64;

A15: (s1 . m) #Q p <> 0 by A4, Th52;

assume m >= n ; :: thesis: contradiction

then |.((s2 . m) - 0).| < d #Q p by A10;

then |.((s1 . m) #Q p).| < d #Q p by A4;

then (s1 . m) #Q p < d #Q p by A13, ABSVALUE:def 1;

hence contradiction by A15, A14, XCMPLX_1:87; :: thesis: verum

end;A11: s1 . m > 0 by A4;

A12: s1 . m <> 0 by A4;

A13: (s1 . m) #Q p > 0 by A4, Th52;

|.(s1 . m).| < d by A7;

then s1 . m < d by A11, ABSVALUE:def 1;

then (s1 . m) / (s1 . m) < d / (s1 . m) by A11, XREAL_1:74;

then 1 <= d / (s1 . m) by A12, XCMPLX_1:60;

then (d / (s1 . m)) #Q p <= 1 by A5, Th61;

then (d #Q p) / ((s1 . m) #Q p) <= 1 by A6, A11, Th58;

then A14: ((d #Q p) / ((s1 . m) #Q p)) * ((s1 . m) #Q p) <= 1 * ((s1 . m) #Q p) by A13, XREAL_1:64;

A15: (s1 . m) #Q p <> 0 by A4, Th52;

assume m >= n ; :: thesis: contradiction

then |.((s2 . m) - 0).| < d #Q p by A10;

then |.((s1 . m) #Q p).| < d #Q p by A4;

then (s1 . m) #Q p < d #Q p by A13, ABSVALUE:def 1;

hence contradiction by A15, A14, XCMPLX_1:87; :: thesis: verum

now :: thesis: for n being Nat holds s2 . n <> 0

then A16:
s2 is non-zero
by SEQ_1:5;let n be Nat; :: thesis: s2 . n <> 0

(s1 . n) #Q p <> 0 by A4, Th52;

hence s2 . n <> 0 by A4; :: thesis: verum

end;(s1 . n) #Q p <> 0 by A4, Th52;

hence s2 . n <> 0 by A4; :: thesis: verum

then A17: lim (s2 ") = (lim s2) " by A2, A9, SEQ_2:22;

deffunc H

consider s being Real_Sequence such that

A18: for n being Nat holds s . n = H

A19: now :: thesis: for n being Nat holds

( s1 . n > 0 & s . n = (s1 . n) #Q (- p) )

A20:
dom s2 = NAT
by FUNCT_2:def 1;( s1 . n > 0 & s . n = (s1 . n) #Q (- p) )

let n be Nat; :: thesis: ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) )

s . n = (s2 . n) " by A18

.= ((s1 . n) #Q p) " by A4

.= 1 / ((s1 . n) #Q p)

.= (s1 . n) #Q (- p) by A4, Th54 ;

hence ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) ) by A4; :: thesis: verum

end;s . n = (s2 . n) " by A18

.= ((s1 . n) #Q p) " by A4

.= 1 / ((s1 . n) #Q p)

.= (s1 . n) #Q (- p) by A4, Th54 ;

hence ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) ) by A4; :: thesis: verum

A21: dom s = NAT by FUNCT_2:def 1;

for n being object st n in dom s holds

s . n = (s2 . n) " by A18;

then A22: s = s2 " by A21, A20, VALUED_1:def 7;

s2 " is convergent by A2, A16, A9, SEQ_2:21;

then (lim s2) " = (lim s1) #Q (- p) by A1, A3, A5, A17, A22, A19, Lm10;

then 1 / (lim s2) = 1 / ((lim s1) #Q p) by A3, Th54;

hence lim s2 = (lim s1) #Q p by XCMPLX_1:59; :: thesis: verum