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;

( 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 )
;

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 ;

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;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

then
(a #Q s1) - (a #Q s2) is convergent
by SEQ_2:def 6;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;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

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