let s, s9 be Complex_Sequence; :: thesis: ( s is convergent Complex_Sequence & s9 is convergent Complex_Sequence implies s (#) s9 is convergent )
assume that
A1: s is convergent Complex_Sequence and
A2: s9 is convergent Complex_Sequence ; :: thesis: s (#) s9 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
|.((s9 . 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 (#) s9) . m) - g).| < p
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 (#) s9) . 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 + 0 < |.g2.| + R by A5, COMPLEX1:46, XREAL_1:8;
assume A8: 0 < p ; :: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - g).| < p
then consider n1 being Element of NAT such that
A9: for m being Element of NAT st n1 <= m holds
|.((s . m) - g1).| < p / (|.g2.| + R) by A3, A7, XREAL_1:139;
consider n2 being Element of NAT such that
A10: for m being Element of NAT st n2 <= m holds
|.((s9 . m) - g2).| < p / (|.g2.| + R) by A4, A7, A8, XREAL_1:139;
take n = n1 + n2; :: thesis: for m being Element of NAT st n <= m holds
|.(((s (#) s9) . m) - g).| < p
let m be Element of NAT ; :: thesis: ( n <= m implies |.(((s (#) s9) . m) - g).| < p )
assume A11: n <= m ; :: thesis: |.(((s (#) s9) . m) - g).| < p
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A11, XXREAL_0:2;
then A12: |.((s . m) - g1).| <= p / (|.g2.| + R) by A9;
( 0 <= |.g2.| & |.(((s . m) - g1) * g2).| = |.g2.| * |.((s . m) - g1).| ) by COMPLEX1:46, COMPLEX1:65;
then A13: |.(((s . m) - g1) * g2).| <= |.g2.| * (p / (|.g2.| + R)) by A12, XREAL_1:64;
|.(((s (#) s9) . m) - g).| = |.(((((s . m) * (s9 . m)) - ((s . m) * g2)) + ((s . m) * g2)) - (g1 * g2)).| by VALUED_1:5
.= |.(((s . m) * ((s9 . m) - g2)) + (((s . m) - g1) * g2)).| ;
then A14: |.(((s (#) s9) . m) - g).| <= |.((s . m) * ((s9 . m) - g2)).| + |.(((s . m) - g1) * g2).| by COMPLEX1:56;
n2 <= n by NAT_1:12;
then n2 <= m by A11, XXREAL_0:2;
then A15: |.((s9 . m) - g2).| < p / (|.g2.| + R) by A10;
A16: ( 0 <= |.(s . m).| & 0 <= |.((s9 . m) - g2).| ) by COMPLEX1:46;
|.(s . m).| < R by A6;
then |.(s . m).| * |.((s9 . m) - g2).| < R * (p / (|.g2.| + R)) by A16, A15, XREAL_1:96;
then A17: |.((s . m) * ((s9 . m) - g2)).| < R * (p / (|.g2.| + R)) by COMPLEX1:65;
(R * (p / (|.g2.| + R))) + (|.g2.| * (p / (|.g2.| + R))) = (p / (|.g2.| + R)) * (|.g2.| + R)
.= p by A7, XCMPLX_1:87 ;
then |.((s . m) * ((s9 . m) - g2)).| + |.(((s . m) - g1) * g2).| < p by A17, A13, XREAL_1:8;
hence |.(((s (#) s9) . m) - g).| < p by A14, XXREAL_0:2; :: thesis: verum