let s1, s2 be Rational_Sequence; :: thesis: for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 holds
( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
let a be real number ; :: thesis: ( s1 is convergent & s2 is convergent & lim s1 = lim s2 & a > 0 implies ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) ) )
assume that
A1: ( s1 is convergent & s2 is convergent & lim s1 = lim s2 ) and
A2: a > 0 ; :: thesis: ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
thus A3: a #Q s1 is convergent by A1, A2, Th82; :: thesis: ( a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
thus A4: a #Q s2 is convergent by A1, A2, Th82; :: thesis: lim (a #Q s1) = lim (a #Q s2)
s1 is bounded by A1, SEQ_2:27;
then consider d being real number such that
A5: ( 0 < d & ( for n being Element of NAT holds abs (s1 . n) < d ) ) by SEQ_2:15;
s2 is bounded by A1, SEQ_2:27;
then consider e being real number such that
A6: ( 0 < e & ( for n being Element of NAT holds abs (s2 . n) < e ) ) by SEQ_2:15;
consider m1 being Element of NAT such that
A7: d + e < m1 by SEQ_4:10;
reconsider m1 = m1 as Rational ;
A8: a #Q m1 > 0 by A2, Th63;

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

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

hence lim (a #Q s1) = lim (a #Q s2) by A1, Lm6; :: thesis: verum

end;

suppose A9: a < 1 ; :: thesis: lim (a #Q s1) = lim (a #Q s2)

then a / a < 1 / a by A2, XREAL_1:76;
then A10: 1 < 1 / a by A2, XCMPLX_1:60;
then A11: lim ((1 / a) #Q s1) = lim ((1 / a) #Q s2) by A1, Lm6;
A12: (1 / a) #Q s1 is convergent by A1, A10, Th82;
A13: (1 / a) #Q s2 is convergent by A1, A10, Th82;
then A14: ((1 / a) #Q s1) - ((1 / a) #Q s2) is convergent by A12, SEQ_2:25;
A15: lim (((1 / a) #Q s1) - ((1 / a) #Q s2)) = (lim ((1 / a) #Q s1)) - (lim ((1 / a) #Q s2)) by A12, A13, SEQ_2:26
.= 0 by A11 ;

A16: now

let c be real number ; :: thesis: ( c > 0 implies ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0 ) < c )
assume A17: c > 0 ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0 ) < c
then c * (a #Q m1) > 0 by A8, XREAL_1:131;
then consider n being Element of NAT such that
A18: for m being Element of NAT st n <= m holds
abs (((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0 ) < c * (a #Q m1) by A14, A15, SEQ_2:def 7;
take n = n; :: thesis: for m being Element of NAT st m >= n holds
abs ((((a #Q s1) - (a #Q s2)) . m) - 0 ) < c
let m be Element of NAT ; :: thesis: ( m >= n implies abs ((((a #Q s1) - (a #Q s2)) . m) - 0 ) < c )
assume m >= n ; :: thesis: abs ((((a #Q s1) - (a #Q s2)) . m) - 0 ) < c
then abs (((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0 ) < c * (a #Q m1) by A18;
then A19: abs ((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)) < c * (a #Q m1) by RFUNCT_2:6;
A20: a #Q (s1 . m) <> 0 by A2, Th63;
A21: a #Q (s2 . m) <> 0 by A2, Th63;
A22: a #Q ((s1 . m) + (s2 . m)) > 0 by A2, Th63;
A23: a #Q ((s1 . m) + (s2 . m)) <> 0 by A2, Th63;
abs ((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)) = abs (((1 / a) #Q (s1 . m)) - (((1 / a) #Q s2) . m)) by Def7
.= abs (((1 / a) #Q (s1 . m)) - ((1 / a) #Q (s2 . m))) by Def7
.= abs ((1 / (a #Q (s1 . m))) - ((1 / a) #Q (s2 . m))) by A2, Th68
.= abs ((1 / (a #Q (s1 . m))) - (1 / (a #Q (s2 . m)))) by A2, Th68
.= abs (((a #Q (s1 . m)) " ) - (1 / (a #Q (s2 . m))))
.= abs (((a #Q (s1 . m)) " ) - ((a #Q (s2 . m)) " ))
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / ((abs (a #Q (s1 . m))) * (abs (a #Q (s2 . m)))) by A20, A21, SEQ_2:11
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (abs ((a #Q (s1 . m)) * (a #Q (s2 . m)))) by COMPLEX1:151
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (abs (a #Q ((s1 . m) + (s2 . m)))) by A2, Th64
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q ((s1 . m) + (s2 . m))) by A22, ABSVALUE:def 1 ;
then ((abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q ((s1 . m) + (s2 . m)))) * (a #Q ((s1 . m) + (s2 . m))) < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m))) by A19, A22, XREAL_1:70;
then A24: abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m))) by A23, XCMPLX_1:88;
abs (s1 . m) < d by A5;
then A25: (abs (s1 . m)) + (abs (s2 . m)) < d + e by A6, XREAL_1:10;
abs ((s1 . m) + (s2 . m)) <= (abs (s1 . m)) + (abs (s2 . m)) by COMPLEX1:142;
then abs ((s1 . m) + (s2 . m)) < d + e by A25, XXREAL_0:2;
then abs ((s1 . m) + (s2 . m)) < m1 by A7, XXREAL_0:2;
then A26: abs (- ((s1 . m) + (s2 . m))) < m1 by COMPLEX1:138;
- ((s1 . m) + (s2 . m)) <= abs (- ((s1 . m) + (s2 . m))) by ABSVALUE:11;
then - ((s1 . m) + (s2 . m)) < m1 by A26, XXREAL_0:2;
then A27: m1 - (- ((s1 . m) + (s2 . m))) > 0 by XREAL_1:52;
(a #Q m1) * (a #Q ((s1 . m) + (s2 . m))) = a #Q (m1 + ((s1 . m) + (s2 . m))) by A2, Th64;
then c * ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m)))) < 1 * c by A2, A9, A17, A27, Th76, XREAL_1:70;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < c by A24, XXREAL_0:2;
then abs (((a #Q s1) . m) - (a #Q (s2 . m))) < c by Def7;
then abs (((a #Q s1) . m) - ((a #Q s2) . m)) < c by Def7;
hence abs ((((a #Q s1) - (a #Q s2)) . m) - 0 ) < c by RFUNCT_2:6; :: thesis: verum

end;

then (a #Q s1) - (a #Q s2) is convergent by SEQ_2:def 6;
then lim ((a #Q s1) - (a #Q s2)) = 0 by A16, SEQ_2:def 7;
then 0 = (lim (a #Q s1)) - (lim (a #Q s2)) by A3, A4, SEQ_2:26;
hence lim (a #Q s1) = lim (a #Q s2) ; :: thesis: verum

end;

end;