let s, s' be Complex_Sequence; :: thesis: ( s is convergent Complex_Sequence & s' is convergent Complex_Sequence implies s (#) s' is convergent )
assume that
A1: s is convergent Complex_Sequence and
A2: s' is convergent Complex_Sequence ; :: thesis: s (#) s' is convergent
consider g1 being Element of COMPLEX such that
A3: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s . m) - g1).| < p by A1, Def4;
consider g2 being Element of COMPLEX such that
A4: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s' . m) - g2).| < p by A2, Def4;
take g = g1 * g2; :: according to COMSEQ_2:def 4 :: thesis: for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s') . m) - g).| < p
consider R being Real such that
A5: 0 < R and
A6: for n being Element of NAT holds |.(s . n).| < R by A1, Th8;
A7: 0 <= |.g2.| by COMPLEX1:132;
A8: 0 + 0 < |.g2.| + R by A5, COMPLEX1:132, XREAL_1:10;
let p be Real; :: thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s') . 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
|.(((s (#) s') . m) - g).| < p
then consider n1 being Element of NAT such that
A10: for m being Element of NAT st n1 <= m holds
|.((s . m) - g1).| < p / (|.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
|.((s' . m) - g2).| < p / (|.g2.| + R) by A4, A9, A8, XREAL_1:141;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s') . m) - g).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s (#) s') . m) - g).| < p )
assume A12: n <= m ; :: thesis: |.(((s (#) s') . m) - g).| < p
A13: 0 <= |.(s . m).| by COMPLEX1:132;
A14: 0 <= |.((s' . m) - g2).| by COMPLEX1:132;
n2 <= n by NAT_1:12;
then n2 <= m by A12, XXREAL_0:2;
then A15: |.((s' . m) - g2).| < p / (|.g2.| + R) by A11;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A12, XXREAL_0:2;
then A16: |.((s . m) - g1).| <= p / (|.g2.| + R) by A10;
|.(((s (#) s') . m) - g).| = |.(((((s . m) * (s' . m)) - ((s . m) * g2)) + ((s . m) * g2)) - (g1 * g2)).| by VALUED_1:5
.= |.(((s . m) * ((s' . m) - g2)) + (((s . m) - g1) * g2)).| ;
then A17: |.(((s (#) s') . m) - g).| <= |.((s . m) * ((s' . m) - g2)).| + |.(((s . m) - g1) * g2).| by COMPLEX1:142;
|.(s . m).| < R by A6;
then |.(s . m).| * |.((s' . m) - g2).| < R * (p / (|.g2.| + R)) by A13, A14, A15, XREAL_1:98;
then A18: |.((s . m) * ((s' . m) - g2)).| < R * (p / (|.g2.| + R)) by COMPLEX1:151;
|.(((s . m) - g1) * g2).| = |.g2.| * |.((s . m) - g1).| by COMPLEX1:151;
then A19: |.(((s . m) - g1) * g2).| <= |.g2.| * (p / (|.g2.| + R)) by A7, A16, XREAL_1:66;
(R * (p / (|.g2.| + R))) + (|.g2.| * (p / (|.g2.| + R))) = (p / (|.g2.| + R)) * (|.g2.| + R)
.= p by A8, XCMPLX_1:88 ;
then |.((s . m) * ((s' . m) - g2)).| + |.(((s . m) - g1) * g2).| < p by A18, A19, XREAL_1:10;
hence |.(((s (#) s') . m) - g).| < p by A17, XXREAL_0:2; :: thesis: verum