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 & s2 is convergent ) and
A2: lim s1 > 0 and
A3: 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, Lm9; :: thesis: verum

end;

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

then A5: - p >= - 0 ;
deffunc H₁( Element of NAT ) -> Element of REAL = (s2 . $1) " ;
consider s being Real_Sequence such that
A6: for n being Element of NAT holds s . n = H₁(n) from SEQ_1:sch 1();

now

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

end;

then A7: s2 is non-zero by SEQ_1:7;
s1 is bounded by A1, SEQ_2:27;
then consider d being real number such that
A8: ( d > 0 & ( for n being Element of NAT holds abs (s1 . n) < d ) ) by SEQ_2:15;
reconsider d = d as Real by XREAL_0:def 1;
A9: d #Q p > 0 by A8, Th63;

A10: now

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

now

let m be Element of NAT ; :: thesis: not m >= n
assume m >= n ; :: thesis: contradiction
then abs ((s2 . m) - 0 ) < d #Q p by A11;
then A12: abs ((s1 . m) #Q p) < d #Q p by A3;
A13: s1 . m > 0 by A3;
then A14: (s1 . m) #Q p > 0 by Th63;
then A15: (s1 . m) #Q p < d #Q p by A12, ABSVALUE:def 1;
A16: s1 . m <> 0 by A3;
A17: (s1 . m) #Q p <> 0 by A13, Th63;
abs (s1 . m) < d by A8;
then s1 . m < d by A13, ABSVALUE:def 1;
then (s1 . m) / (s1 . m) < d / (s1 . m) by A13, XREAL_1:76;
then 1 <= d / (s1 . m) by A16, XCMPLX_1:60;
then (d / (s1 . m)) #Q p <= 1 by A4, Th72;
then (d #Q p) / ((s1 . m) #Q p) <= 1 by A8, A13, Th69;
then ((d #Q p) / ((s1 . m) #Q p)) * ((s1 . m) #Q p) <= 1 * ((s1 . m) #Q p) by A14, XREAL_1:66;
hence contradiction by A15, A17, XCMPLX_1:88; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

then A18: s2 " is convergent by A1, A7, SEQ_2:35;
A19: lim (s2 " ) = (lim s2) " by A1, A7, A10, SEQ_2:36;
A20: dom s = NAT by FUNCT_2:def 1;
A21: dom s2 = NAT by FUNCT_2:def 1;
for n being set st n in dom s holds
s . n = (s2 . n) " by A6, A20;
then A22: s = s2 " by A20, A21, VALUED_1:def 7;

now

let n be Element of NAT ; :: thesis: ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) )
A23: s1 . n > 0 by A3;
s . n = (s2 . n) " by A6
.= ((s1 . n) #Q p) " by A3
.= 1 / ((s1 . n) #Q p)
.= (s1 . n) #Q (- p) by A23, Th65 ;
hence ( s1 . n > 0 & s . n = (s1 . n) #Q (- p) ) by A3; :: thesis: verum

end;

then (lim s2) " = (lim s1) #Q (- p) by A1, A2, A5, A18, A19, A22, Lm9;
then 1 / (lim s2) = (lim s1) #Q (- p) ;
then 1 / (lim s2) = 1 / ((lim s1) #Q p) by A2, Th65;
hence lim s2 = (lim s1) #Q p by XCMPLX_1:59; :: thesis: verum

end;

end;