let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: seq (#) seq9 is convergent
consider g1 being real number such that
A3: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq . m) - g1) < p by A1, Def6;
consider g2 being real number such that
A4: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((seq9 . m) - g2) < p by A2, Def6;
take g = g1 * g2; :: according to SEQ_2:def 6 :: thesis: for p being real number st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p
seq is bounded by A1, Th27;
then consider r being real number such that
A5: 0 < r and
A6: for n being Element of NAT holds abs (seq . n) < r by Th15;
A7: 0 <= abs g2 by COMPLEX1:132;
A8: 0 + 0 < (abs g2) + r by A5, COMPLEX1:132, XREAL_1:10;
let p be real number ; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p )
assume A9: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p
then consider n1 being Element of NAT such that
A10: for m being Element of NAT st n1 <= m holds
abs ((seq . m) - g1) < p / ((abs g2) + r) by A3, A8, XREAL_1:141;
consider n2 being Element of NAT such that
A11: for m being Element of NAT st n2 <= m holds
abs ((seq9 . m) - g2) < p / ((abs g2) + r) by A4, A8, A9, XREAL_1:141;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
abs (((seq (#) seq9) . m) - g) < p
let m be Element of NAT ; :: thesis: ( n <= m implies abs (((seq (#) seq9) . m) - g) < p )
assume A12: n <= m ; :: thesis: abs (((seq (#) seq9) . m) - g) < p
A13: 0 <= abs (seq . m) by COMPLEX1:132;
A14: 0 <= abs ((seq9 . m) - g2) by COMPLEX1:132;
n2 <= n by NAT_1:12;
then n2 <= m by A12, XXREAL_0:2;
then A15: abs ((seq9 . m) - g2) < p / ((abs g2) + r) by A11;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A12, XXREAL_0:2;
then A16: abs ((seq . m) - g1) <= p / ((abs g2) + r) by A10;
abs (((seq (#) seq9) . m) - g) = abs ((((seq . m) * (seq9 . m)) - (((seq . m) * g2) - ((seq . m) * g2))) - (g1 * g2)) by SEQ_1:12
.= abs (((seq . m) * ((seq9 . m) - g2)) + (((seq . m) - g1) * g2)) ;
then A17: abs (((seq (#) seq9) . m) - g) <= (abs ((seq . m) * ((seq9 . m) - g2))) + (abs (((seq . m) - g1) * g2)) by COMPLEX1:142;
abs (seq . m) < r by A6;
then (abs (seq . m)) * (abs ((seq9 . m) - g2)) < r * (p / ((abs g2) + r)) by A13, A14, A15, XREAL_1:98;
then A18: abs ((seq . m) * ((seq9 . m) - g2)) < r * (p / ((abs g2) + r)) by COMPLEX1:151;
abs (((seq . m) - g1) * g2) = (abs g2) * (abs ((seq . m) - g1)) by COMPLEX1:151;
then A19: abs (((seq . m) - g1) * g2) <= (abs g2) * (p / ((abs g2) + r)) by A7, A16, XREAL_1:66;
(r * (p / ((abs g2) + r))) + ((abs g2) * (p / ((abs g2) + r))) = (p / ((abs g2) + r)) * ((abs g2) + r)
.= p by A8, XCMPLX_1:88 ;
then (abs ((seq . m) * ((seq9 . m) - g2))) + (abs (((seq . m) - g1) * g2)) < p by A18, A19, XREAL_1:10;
hence abs (((seq (#) seq9) . m) - g) < p by A17, XXREAL_0:2; :: thesis: verum