let a be Real; :: thesis: for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) holds
lim s2 = a #R (lim s1)
let s1, s2 be Real_Sequence; :: thesis: ( a > 0 & s1 is convergent & s2 is convergent & ( for n being Nat holds s2 . n = a #R (s1 . n) ) implies lim s2 = a #R (lim s1) )
assume that
A1: a > 0 and
A2: s1 is convergent and
A3: s2 is convergent and
A4: for n being Nat holds s2 . n = a #R (s1 . n) ; :: thesis: lim s2 = a #R (lim s1)

per cases ( a >= 1 or a < 1 ) ;

suppose a >= 1 ; :: thesis: lim s2 = a #R (lim s1)

hence lim s2 = a #R (lim s1) by A2, A3, A4, Lm12; :: thesis: verum

end;

suppose A5: a < 1 ; :: thesis: lim s2 = a #R (lim s1)

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

assume A7: lim s2 = 0 ; :: thesis: contradiction
a #R ((lim s1) + 1) > 0 by A1, Th81;
then consider n being Nat such that
A8: for m being Nat st m >= n holds
|.((s2 . m) - 0).| < a #R ((lim s1) + 1) by A3, A7, SEQ_2:def 7;
consider n1 being Nat such that
A9: for m being Nat st m >= n1 holds
|.((s1 . m) - (lim s1)).| < 1 by A2, SEQ_2:def 7;

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

let m be Nat; :: thesis: not m >= n + n1
assume A10: m >= n + n1 ; :: thesis: contradiction
n + n1 >= n1 by NAT_1:12;
then m >= n1 by A10, XXREAL_0:2;
then A11: |.((s1 . m) - (lim s1)).| < 1 by A9;
(s1 . m) - (lim s1) <= |.((s1 . m) - (lim s1)).| by ABSVALUE:4;
then (s1 . m) - (lim s1) < 1 by A11, XXREAL_0:2;
then A12: ((s1 . m) - (lim s1)) + (lim s1) < (lim s1) + 1 by XREAL_1:6;
n + n1 >= n by NAT_1:12;
then m >= n by A10, XXREAL_0:2;
then |.((s2 . m) - 0).| < a #R ((lim s1) + 1) by A8;
then A13: |.(a #R (s1 . m)).| < a #R ((lim s1) + 1) by A4;
a #R (s1 . m) > 0 by A1, Th81;
then a #R (s1 . m) < a #R ((lim s1) + 1) by A13, ABSVALUE:def 1;
hence contradiction by A1, A5, A12, Th84; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

A14: now :: thesis: for n being Nat holds (s2 ") . n = (1 / a) #R (s1 . n)

let n be Nat; :: thesis: (s2 ") . n = (1 / a) #R (s1 . n)
thus (s2 ") . n = (s2 . n) " by VALUED_1:10
.= (a #R (s1 . n)) " by A4
.= 1 / (a #R (s1 . n))
.= (1 / a) #R (s1 . n) by A1, Th79 ; :: thesis: verum

end;

a * (1 / a) <= 1 * (1 / a) by A1, A5, XREAL_1:64;
then A15: 1 <= 1 / a by A1, XCMPLX_1:106;
A16: a #R (lim s1) <> 0 by A1, Th81;

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

let n be Nat; :: thesis: s2 . n <> 0
s2 . n = a #R (s1 . n) by A4;
hence s2 . n <> 0 by A1, Th81; :: thesis: verum

end;

then A17: s2 is non-zero by SEQ_1:5;
then A18: lim (s2 ") = (lim s2) " by A3, A6, SEQ_2:22;
s2 " is convergent by A3, A6, A17, SEQ_2:21;
then (lim s2) " = (1 / a) #R (lim s1) by A2, A15, A18, A14, Lm12
.= 1 / (a #R (lim s1)) by A1, Th79 ;
then 1 = (1 / (a #R (lim s1))) * (lim s2) by A6, XCMPLX_0:def 7;
then a #R (lim s1) = (a #R (lim s1)) * ((1 / (a #R (lim s1))) * (lim s2))
.= ((a #R (lim s1)) * (1 / (a #R (lim s1)))) * (lim s2)
.= 1 * (lim s2) by A16, XCMPLX_1:106 ;
hence lim s2 = a #R (lim s1) ; :: thesis: verum

end;

end;