let a be real number ; :: thesis: for s1, s2 being Real_Sequence st a > 0 & s1 is convergent & s2 is convergent & ( for n being Element of 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 Element of 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 & s2 is convergent ) and
A3: for n being Element of NAT holds s2 . n = a #R (s1 . n) ; :: thesis: lim s2 = a #R (lim s1)
a " > 0 by A1;
then A4: 1 / a >= 0 ;

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, Lm11; :: thesis: verum

end;

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

then a * (1 / a) <= 1 * (1 / a) by A4, XREAL_1:66;
then A6: 1 <= 1 / a by A1, XCMPLX_1:107;

A7: now

assume A8: lim s2 = 0 ; :: thesis: contradiction
a #R ((lim s1) + 1) > 0 by A1, Th95;
then consider n being Element of NAT such that
A9: for m being Element of NAT st m >= n holds
abs ((s2 . m) - 0 ) < a #R ((lim s1) + 1) by A2, A8, SEQ_2:def 7;
consider n1 being Element of NAT such that
A10: for m being Element of NAT st m >= n1 holds
abs ((s1 . m) - (lim s1)) < 1 by A2, SEQ_2:def 7;

now

let m be Element of NAT ; :: thesis: not m >= n + n1
assume A11: m >= n + n1 ; :: thesis: contradiction
n + n1 >= n by NAT_1:12;
then A12: m >= n by A11, XXREAL_0:2;
n + n1 >= n1 by NAT_1:12;
then A13: m >= n1 by A11, XXREAL_0:2;
A14: a #R (s1 . m) > 0 by A1, Th95;
abs ((s2 . m) - 0 ) < a #R ((lim s1) + 1) by A9, A12;
then abs (a #R (s1 . m)) < a #R ((lim s1) + 1) by A3;
then A15: a #R (s1 . m) < a #R ((lim s1) + 1) by A14, ABSVALUE:def 1;
A16: abs ((s1 . m) - (lim s1)) < 1 by A10, A13;
(s1 . m) - (lim s1) <= abs ((s1 . m) - (lim s1)) by ABSVALUE:11;
then (s1 . m) - (lim s1) < 1 by A16, XXREAL_0:2;
then ((s1 . m) - (lim s1)) + (lim s1) < (lim s1) + 1 by XREAL_1:8;
hence contradiction by A1, A5, A15, Th98; :: thesis: verum

end;

hence contradiction ; :: thesis: verum

end;

now

let n be Element of NAT ; :: thesis: s2 . n <> 0
s2 . n = a #R (s1 . n) by A3;
hence s2 . n <> 0 by A1, Th95; :: thesis: verum

end;

then A17: s2 is non-zero by SEQ_1:7;
then A18: s2 " is convergent by A2, A7, SEQ_2:35;
A19: lim (s2 " ) = (lim s2) " by A2, A7, A17, SEQ_2:36;
A20: a #R (lim s1) <> 0 by A1, Th95;

now

let n be Element of NAT ; :: thesis: (s2 " ) . n = (1 / a) #R (s1 . n)
thus (s2 " ) . n = (s2 . n) " by VALUED_1:10
.= (a #R (s1 . n)) " by A3
.= 1 / (a #R (s1 . n))
.= (1 / a) #R (s1 . n) by A1, Th93 ; :: thesis: verum

end;

then (lim s2) " = (1 / a) #R (lim s1) by A2, A6, A18, A19, Lm11
.= 1 / (a #R (lim s1)) by A1, Th93 ;
then 1 = (1 / (a #R (lim s1))) * (lim s2) by A7, 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 A20, XCMPLX_1:107 ;
hence lim s2 = a #R (lim s1) ; :: thesis: verum

end;

end;