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 ;
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 ;
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 ;
|.(s1 . m).| < d by A7;
then s1 . m < d by ;
then (s1 . m) / (s1 . m) < d / (s1 . m) by ;
then 1 <= d / (s1 . m) by ;
then (d / (s1 . m)) #Q p <= 1 by ;
then (d #Q p) / ((s1 . m) #Q p) <= 1 by ;
then A14: ((d #Q p) / ((s1 . m) #Q p)) * ((s1 . m) #Q p) <= 1 * ((s1 . m) #Q p) by ;
A15: (s1 . m) #Q p <> 0 by ;
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 ;
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 ;
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 ;
deffunc H1( Nat) -> object = (s2 . \$1) " ;
consider s being Real_Sequence such that
A18: for n being Nat holds s . n = H1(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 ;
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 ;
s2 " is convergent by ;
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 ;
hence lim s2 = (lim s1) #Q p by XCMPLX_1:59; :: thesis: verum
end;
end;