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 ;
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 ;
consider n1 being Nat such that
A9: for m being Nat st m >= n1 holds
|.((s1 . m) - (lim s1)).| < 1 by ;
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 ;
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 ;
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 ;
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 ;
then a #R (s1 . m) < a #R ((lim s1) + 1) by ;
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 ; :: thesis: verum
end;
a * (1 / a) <= 1 * (1 / a) by ;
then A15: 1 <= 1 / a by ;
A16: a #R (lim s1) <> 0 by ;
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 ; :: thesis: verum
end;
then A17: s2 is non-zero by SEQ_1:5;
then A18: lim (s2 ") = (lim s2) " by ;
s2 " is convergent by ;
then (lim s2) " = (1 / a) #R (lim s1) by A2, A15, A18, A14, Lm12
.= 1 / (a #R (lim s1)) by ;
then 1 = (1 / (a #R (lim s1))) * (lim s2) by ;
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 ;
hence lim s2 = a #R (lim s1) ; :: thesis: verum
end;
end;