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

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

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

hence lim s2 = (lim s1) #Q p by A1, A2, A3, A4, Lm10; :: thesis: verum

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;

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;

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

let 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;

hence contradiction ; :: thesis: verum

end;

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

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;

then A16: s2 is non-zero by SEQ_1:5;
then A17: lim (s2 ") = (lim s2) " by A2, A9, SEQ_2:22;
deffunc H₁( Nat) -> object = (s2 . $1) " ;
consider s being Real_Sequence such that
A18: for n being Nat holds s . n = H₁(n) from SEQ_1:sch 1();

A19: now :: thesis: for n being Nat holds
( 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;

A20: dom s2 = NAT by FUNCT_2:def 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;

end;