let s1, s2 be Rational_Sequence; :: thesis: for a being Real 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; :: 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, Th69; :: thesis: ( a #Q s2 is convergent & lim (a #Q s1) = lim (a #Q s2) )
s2 is bounded by A2;
then consider e being Real such that
0 < e and
A6: for n being Nat holds |.(s2 . n).| < e by SEQ_2:3;
s1 is bounded by A1;
then consider d being Real such that
0 < d and
A7: for n being Nat holds |.(s1 . n).| < d by SEQ_2:3;
consider m1 being Nat such that
A8: d + e < m1 by SEQ_4:3;
thus A9: a #Q s2 is convergent by A2, A4, Th69; :: thesis: lim (a #Q s1) = lim (a #Q s2)
reconsider m1 = m1 as Rational ;
A10: a #Q m1 > 0 by A4, Th52;

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:74;
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, Th69;
A14: (1 / a) #Q s1 is convergent by A1, A4, Th69;
then A15: ((1 / a) #Q s1) - ((1 / a) #Q s2) is convergent by A13;
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:12
.= 0 by A12 ;

A17: now :: thesis: for c being Real st c > 0 holds
ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c

let c be Real; :: thesis: ( c > 0 implies ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c )
assume A18: c > 0 ; :: thesis: ex n being Nat st
for m being Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c
then c * (a #Q m1) > 0 by A10;
then consider n being Nat such that
A19: for m being Nat st n <= m holds
|.(((((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 Nat st m >= n holds
|.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c
let m be Nat; :: thesis: ( m >= n implies |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c )
assume m >= n ; :: thesis: |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c
then |.(((((1 / a) #Q s1) - ((1 / a) #Q s2)) . m) - 0).| < c * (a #Q m1) by A19;
then A20: |.((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)).| < c * (a #Q m1) by RFUNCT_2:1;
A21: a #Q (s1 . m) <> 0 by A4, Th52;
|.(s1 . m).| < d by A7;
then A22: |.(s1 . m).| + |.(s2 . m).| < d + e by A6, XREAL_1:8;
|.((s1 . m) + (s2 . m)).| <= |.(s1 . m).| + |.(s2 . m).| by COMPLEX1:56;
then |.((s1 . m) + (s2 . m)).| < d + e by A22, XXREAL_0:2;
then |.((s1 . m) + (s2 . m)).| < m1 by A8, XXREAL_0:2;
then A23: |.(- ((s1 . m) + (s2 . m))).| < m1 by COMPLEX1:52;
- ((s1 . m) + (s2 . m)) <= |.(- ((s1 . m) + (s2 . m))).| by ABSVALUE:4;
then - ((s1 . m) + (s2 . m)) < m1 by A23, XXREAL_0:2;
then A24: m1 - (- ((s1 . m) + (s2 . m))) > 0 by XREAL_1:50;
A25: a #Q (s2 . m) <> 0 by A4, Th52;
A26: a #Q ((s1 . m) + (s2 . m)) > 0 by A4, Th52;
|.((((1 / a) #Q s1) . m) - (((1 / a) #Q s2) . m)).| = |.(((1 / a) #Q (s1 . m)) - (((1 / a) #Q s2) . m)).| by Def5
.= |.(((1 / a) #Q (s1 . m)) - ((1 / a) #Q (s2 . m))).| by Def5
.= |.((1 / (a #Q (s1 . m))) - ((1 / a) #Q (s2 . m))).| by A4, Th57
.= |.((1 / (a #Q (s1 . m))) - (1 / (a #Q (s2 . m)))).| by A4, Th57
.= |.(((a #Q (s1 . m)) ") - (1 / (a #Q (s2 . m)))).|
.= |.(((a #Q (s1 . m)) ") - ((a #Q (s2 . m)) ")).|
.= |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (|.(a #Q (s1 . m)).| * |.(a #Q (s2 . m)).|) by A21, A25, SEQ_2:2
.= |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / |.((a #Q (s1 . m)) * (a #Q (s2 . m))).| by COMPLEX1:65
.= |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / |.(a #Q ((s1 . m) + (s2 . m))).| by A4, Th53
.= |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| / (a #Q ((s1 . m) + (s2 . m))) by A26, ABSVALUE:def 1 ;
then A27: (|.((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:68;
a #Q ((s1 . m) + (s2 . m)) <> 0 by A4, Th52;
then A28: |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < (c * (a #Q m1)) * (a #Q ((s1 . m) + (s2 . m))) by A27, XCMPLX_1:87;
(a #Q m1) * (a #Q ((s1 . m) + (s2 . m))) = a #Q (m1 + ((s1 . m) + (s2 . m))) by A4, Th53;
then c * ((a #Q m1) * (a #Q ((s1 . m) + (s2 . m)))) < 1 * c by A4, A11, A18, A24, Th65, XREAL_1:68;
then |.((a #Q (s1 . m)) - (a #Q (s2 . m))).| < c by A28, XXREAL_0:2;
then |.(((a #Q s1) . m) - (a #Q (s2 . m))).| < c by Def5;
then |.(((a #Q s1) . m) - ((a #Q s2) . m)).| < c by Def5;
hence |.((((a #Q s1) - (a #Q s2)) . m) - 0).| < c by RFUNCT_2:1; :: 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:12;
hence lim (a #Q s1) = lim (a #Q s2) ; :: thesis: verum

end;

end;