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 and
A2: s2 is convergent and
A3: lim s1 = lim s2 and
A4: a > 0 ; :: thesis: ( a #Q s1 is convergent & a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
thus A5: a #Q s1 is convergent by A1, A4, Th82; :: thesis: ( a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
s2 is bounded by A2, SEQ_2:27;
then consider e being real number such that
0 < e and
A6: for n being Element of NAT holds abs (s2 . n) < e by SEQ_2:15;
s1 is bounded by A1, SEQ_2:27;
then consider d being real number such that
0 < d and
A7: for n being Element of NAT holds abs (s1 . n) < d by SEQ_2:15;
consider m1 being Element of NAT such that
A8: d + e < m1 by SEQ_4:10;
thus A9: a #Q s2 is convergent by A2, A4, Th82; :: thesis: lim (a #Q s1) = lim (a #Q s2)
reconsider m1 = m1 as Rational ;
A10: a #Q m1 > 0 by A4, 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, A2, A3, Lm7; :: thesis: verum

end;

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

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

A17: 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 A18: 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 A10, XREAL_1:131;
then consider n being Element of NAT such that
A19: 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 A15, A16, 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 A19;
then A20: abs ((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)) < c * (a #Q m1) by RFUNCT_2:6;
A21: a #Q (s1 . m) <> 0 by A4, Th63;
abs (s1 . m) < d by A7;
then A22: (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 A22, XXREAL_0:2;
then abs ((s1 . m) + (s2 . m)) < m1 by A8, XXREAL_0:2;
then A23: 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 A23, XXREAL_0:2;
then A24: m1 - (- ((s1 . m) + (s2 . m))) > 0 by XREAL_1:52;
A25: a #Q (s2 . m) <> 0 by A4, Th63;
A26: a #Q ((s1 . m) + (s2 . m)) > 0 by A4, 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 A4, Th68
.= abs ((1 / (a #Q (s1 . m))) - (1 / (a #Q (s2 . m)))) by A4, 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 A21, A25, 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 A4, Th64
.= (abs ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q ((s1 . m) + (s2 . m))) by A26, ABSVALUE:def 1 ;
then A27: ((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 A20, A26, XREAL_1:70;
a #Q ((s1 . m) + (s2 . m)) <> 0 by A4, Th63;
then A28: abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m))) by A27, XCMPLX_1:88;
(a #Q m1) * (a #Q ((s1 . m) + (s2 . m))) = a #Q (m1 + ((s1 . m) + (s2 . m))) by A4, Th64;
then c * ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m)))) < 1 * c by A4, A11, A18, A24, Th76, XREAL_1:70;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < c by A28, 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 A17, SEQ_2:def 7;
then 0 = (lim (a #Q s1)) - (lim (a #Q s2)) by A5, A9, SEQ_2:26;
hence lim (a #Q s1) = lim (a #Q s2) ; :: thesis: verum

end;

end;