let p be Rational; :: thesis: for s1, s2 being Real_Sequence st s1 is convergent & s2 is convergent & lim s1 > 0 & ( for n being Element of 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 Element of 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 Element of 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, SEQ_2:13;
then consider d being real number such that
A6: d > 0 and
A7: for n being Element of NAT holds abs (s1 . n) < d by SEQ_2:3;
reconsider d = d as Real by XREAL_0:def 1;
A8: d #Q p > 0 by A6, Th63;

A9: now

assume lim s2 = 0 ; :: thesis: contradiction
then consider n being Element of NAT such that
A10: for m being Element of NAT st m >= n holds
abs ((s2 . m) - 0) < d #Q p by A2, A8, SEQ_2:def 7;

now

let m be Element of 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, Th63;
abs (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, Th72;
then (d #Q p) / ((s1 . m) #Q p) <= 1 by A6, A11, Th69;
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, Th63;
assume m >= n ; :: thesis: contradiction
then abs ((s2 . m) - 0) < d #Q p by A10;
then abs ((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

let n be Element of NAT ; :: thesis: s2 . n <> 0
(s1 . n) #Q p <> 0 by A4, Th63;
hence s2 . n <> 0 by A4; :: thesis: verum

end;

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

A19: now

let n be Element of 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, Th65 ;
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;
then for n being set 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, Th65;
hence lim s2 = (lim s1) #Q p by XCMPLX_1:59; :: thesis: verum

end;

end;