let s1, s2 be Rational_Sequence; :: thesis: for a being real number st s1 is convergent & s2 is convergent & lim s1 = lim s2 & a >= 1 holds
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 >= 1 implies 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 >= 1 ; :: thesis: lim (a #Q s1) = lim (a #Q s2)
A5: s1 - s2 is convergent by A1, A2, SEQ_2:25;
A6: a #Q s2 is convergent by A2, A4, Th82;

A7: now

let n be Element of NAT ; :: thesis: (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (a #Q s1) . n
thus (((a #Q s1) - (a #Q s2)) + (a #Q s2)) . n = (((a #Q s1) - (a #Q s2)) . n) + ((a #Q s2) . n) by SEQ_1:11
.= (((a #Q s1) . n) - ((a #Q s2) . n)) + ((a #Q s2) . n) by RFUNCT_2:6
.= (a #Q s1) . n ; :: thesis: verum

end;

s2 is bounded by A2, SEQ_2:27;
then consider d being real number such that
0 < d and
A8: for n being Element of NAT holds abs (s2 . n) < d by SEQ_2:15;
consider m2 being Element of NAT such that
A9: d < m2 by SEQ_4:10;
reconsider m2 = m2 as Rational ;
A10: lim (s1 - s2) = (lim s1) - (lim s2) by A1, A2, SEQ_2:26
.= 0 by A3 ;

A11: now

A12: a #Q m2 >= 0 by A4, Th63;
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 A13: 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
consider m1 being Element of NAT such that
A14: ((a #Q m2) * (a - 1)) / c < m1 by SEQ_4:10;
m1 + 1 >= m1 by XREAL_1:31;
then ((a #Q m2) * (a - 1)) / c < m1 + 1 by A14, XXREAL_0:2;
then (((a #Q m2) * (a - 1)) / c) * c < c * (m1 + 1) by A13, XREAL_1:70;
then (a #Q m2) * (a - 1) < c * (m1 + 1) by A13, XCMPLX_1:88;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < ((m1 + 1) * c) / (m1 + 1) by XREAL_1:76;
then ((a #Q m2) * (a - 1)) / (m1 + 1) < (c / (m1 + 1)) * (m1 + 1) ;
then A15: ((a #Q m2) * (a - 1)) / (m1 + 1) < c by XCMPLX_1:88;
consider n being Element of NAT such that
A16: for m being Element of NAT st n <= m holds
abs (((s1 - s2) . m) - 0 ) < (m1 + 1) " by A5, A10, 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 (((s1 - s2) . m) - 0 ) < (m1 + 1) " by A16;
then A17: abs ((s1 . m) - (s2 . m)) <= (m1 + 1) " by RFUNCT_2:6;
A18: m1 + 1 >= 0 + 1 by NAT_1:13;
then ((m1 + 1) -Root a) - 1 <= (a - 1) / (m1 + 1) by A4, Th40;
then A19: (a #Q m2) * (((m1 + 1) -Root a) - 1) <= (a #Q m2) * ((a - 1) / (m1 + 1)) by A12, XREAL_1:66;
A20: a #Q (s2 . m) <> 0 by A4, Th63;
A21: abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) = abs (((a #Q (s1 . m)) - (a #Q (s2 . m))) * 1)
.= abs (((a #Q (s1 . m)) - (a #Q (s2 . m))) * ((a #Q (s2 . m)) / (a #Q (s2 . m)))) by A20, XCMPLX_1:60
.= abs (((a #Q (s2 . m)) * ((a #Q (s1 . m)) - (a #Q (s2 . m)))) / (a #Q (s2 . m)))
.= abs ((a #Q (s2 . m)) * (((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m))))
.= (abs (a #Q (s2 . m))) * (abs (((a #Q (s1 . m)) - (a #Q (s2 . m))) / (a #Q (s2 . m)))) by COMPLEX1:151
.= (abs (a #Q (s2 . m))) * (abs (((a #Q (s1 . m)) / (a #Q (s2 . m))) - ((a #Q (s2 . m)) / (a #Q (s2 . m)))))
.= (abs (a #Q (s2 . m))) * (abs (((a #Q (s1 . m)) / (a #Q (s2 . m))) - 1)) by A20, XCMPLX_1:60
.= (abs (a #Q (s2 . m))) * (abs ((a #Q ((s1 . m) - (s2 . m))) - 1)) by A4, Th66 ;
A22: s2 . m <= abs (s2 . m) by ABSVALUE:11;
reconsider m3 = (m1 + 1) " as Rational ;
A23: abs ((a #Q ((s1 . m) - (s2 . m))) - 1) >= 0 by COMPLEX1:132;
A24: a #Q ((s1 . m) - (s2 . m)) <> 0 by A4, Th63;
(s1 . m) - (s2 . m) <= abs ((s1 . m) - (s2 . m)) by ABSVALUE:11;
then (s1 . m) - (s2 . m) <= (m1 + 1) " by A17, XXREAL_0:2;
then a #Q ((s1 . m) - (s2 . m)) <= a #Q m3 by A4, Th74;
then a #Q ((s1 . m) - (s2 . m)) <= (m1 + 1) -Root a by A18, Th61;
then A25: (a #Q ((s1 . m) - (s2 . m))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:11;
A26: a #Q ((s1 . m) - (s2 . m)) > 0 by A4, Th63;

A27: now

per cases ( (s1 . m) - (s2 . m) >= 0 or (s1 . m) - (s2 . m) < 0 ) ;

suppose (s1 . m) - (s2 . m) >= 0 ; :: thesis: abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1

then a #Q ((s1 . m) - (s2 . m)) >= 1 by A4, Th71;
then (a #Q ((s1 . m) - (s2 . m))) - 1 >= 0 by XREAL_1:50;
hence abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1 by A25, ABSVALUE:def 1; :: thesis: verum

end;

suppose A28: (s1 . m) - (s2 . m) < 0 ; :: thesis: abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1

A29: - ((s1 . m) - (s2 . m)) <= abs (- ((s1 . m) - (s2 . m))) by ABSVALUE:11;
abs ((s1 . m) - (s2 . m)) = abs (- ((s1 . m) - (s2 . m))) by COMPLEX1:138;
then - ((s1 . m) - (s2 . m)) <= m3 by A17, A29, XXREAL_0:2;
then a #Q (- ((s1 . m) - (s2 . m))) <= a #Q m3 by A4, Th74;
then a #Q (- ((s1 . m) - (s2 . m))) <= (m1 + 1) -Root a by A18, Th61;
then A30: (a #Q (- ((s1 . m) - (s2 . m)))) - 1 <= ((m1 + 1) -Root a) - 1 by XREAL_1:11;
a #Q (- ((s1 . m) - (s2 . m))) >= 1 by A4, A28, Th71;
then (a #Q (- ((s1 . m) - (s2 . m)))) - 1 >= 0 by XREAL_1:50;
then A31: abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1) <= ((m1 + 1) -Root a) - 1 by A30, ABSVALUE:def 1;
a #Q ((s1 . m) - (s2 . m)) <= 1 by A4, A28, Th72;
then A32: abs (a #Q ((s1 . m) - (s2 . m))) <= 1 by A26, ABSVALUE:def 1;
abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1) >= 0 by COMPLEX1:132;
then A33: (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1)) <= 1 * (abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1)) by A32, XREAL_1:66;
abs ((a #Q ((s1 . m) - (s2 . m))) - 1) = abs (((a #Q ((s1 . m) - (s2 . m))) - 1) * 1)
.= abs (((a #Q ((s1 . m) - (s2 . m))) - 1) * ((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m))))) by A24, XCMPLX_1:60
.= abs (((a #Q ((s1 . m) - (s2 . m))) * ((a #Q ((s1 . m) - (s2 . m))) - 1)) / (a #Q ((s1 . m) - (s2 . m))))
.= abs ((a #Q ((s1 . m) - (s2 . m))) * (((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m)))))
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (((a #Q ((s1 . m) - (s2 . m))) - 1) / (a #Q ((s1 . m) - (s2 . m))))) by COMPLEX1:151
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (((a #Q ((s1 . m) - (s2 . m))) / (a #Q ((s1 . m) - (s2 . m)))) - (1 / (a #Q ((s1 . m) - (s2 . m))))))
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (1 - (1 / (a #Q ((s1 . m) - (s2 . m)))))) by A24, XCMPLX_1:60
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (1 - (a #Q (- ((s1 . m) - (s2 . m)))))) by A4, Th65
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs (- (1 - (a #Q (- ((s1 . m) - (s2 . m))))))) by COMPLEX1:138
.= (abs (a #Q ((s1 . m) - (s2 . m)))) * (abs ((a #Q (- ((s1 . m) - (s2 . m)))) - 1)) ;
hence abs ((a #Q ((s1 . m) - (s2 . m))) - 1) <= ((m1 + 1) -Root a) - 1 by A31, A33, XXREAL_0:2; :: thesis: verum

end;

end;

end;

A34: a #Q (s2 . m) > 0 by A4, Th63;
abs (s2 . m) <= m2 by A8, A9, XXREAL_0:2;
then s2 . m <= m2 by A22, XXREAL_0:2;
then a #Q (s2 . m) <= a #Q m2 by A4, Th74;
then A35: abs (a #Q (s2 . m)) <= a #Q m2 by A34, ABSVALUE:def 1;
abs (a #Q (s2 . m)) >= 0 by A34, ABSVALUE:def 1;
then (abs (a #Q (s2 . m))) * (abs ((a #Q ((s1 . m) - (s2 . m))) - 1)) <= (a #Q m2) * (((m1 + 1) -Root a) - 1) by A27, A23, A35, XREAL_1:68;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) <= ((a #Q m2) * (a - 1)) / (m1 + 1) by A21, A19, XXREAL_0:2;
then abs ((a #Q (s1 . m)) - (a #Q (s2 . m))) < c by A15, 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 A36: (a #Q s1) - (a #Q s2) is convergent by SEQ_2:def 6;
then lim ((a #Q s1) - (a #Q s2)) = 0 by A11, SEQ_2:def 7;
then lim (((a #Q s1) - (a #Q s2)) + (a #Q s2)) = 0 + (lim (a #Q s2)) by A36, A6, SEQ_2:20
.= lim (a #Q s2) ;
hence lim (a #Q s1) = lim (a #Q s2) by A7, FUNCT_2:113; :: thesis: verum