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 such that
A3: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g1).| < p by A1;
consider g2 being Real such that
A4: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq9 . m) - g2).| < p by A2;
take g = g1 * g2; :: according to SEQ_2:def 6 :: thesis: for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - g).| < p
consider r being Real such that
A5: 0 < r and
A6: for n being Nat holds |.(seq . n).| < r by A1, Th3;
A7: 0 <= |.g2.| by COMPLEX1:46;
A8: 0 + 0 < |.g2.| + r by A5, COMPLEX1:46, XREAL_1:8;
let p be Real; :: thesis: ( 0 < p implies ex n being Nat st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - g).| < p )
assume A9: 0 < p ; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - g).| < p
then consider n1 being Nat such that
A10: for m being Nat st n1 <= m holds
|.((seq . m) - g1).| < p / (|.g2.| + r) by A3, A8;
consider n2 being Nat such that
A11: for m being Nat st n2 <= m holds
|.((seq9 . m) - g2).| < p / (|.g2.| + r) by A4, A8, A9;
take n = n1 + n2; :: thesis: for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - g).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((seq (#) seq9) . m) - g).| < p )
assume A12: n <= m ; :: thesis: |.(((seq (#) seq9) . m) - g).| < p
A13: 0 <= |.(seq . m).| by COMPLEX1:46;
A14: 0 <= |.((seq9 . m) - g2).| by COMPLEX1:46;
n2 <= n by NAT_1:12;
then n2 <= m by A12, XXREAL_0:2;
then A15: |.((seq9 . m) - g2).| < p / (|.g2.| + r) by A11;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A12, XXREAL_0:2;
then A16: |.((seq . m) - g1).| <= p / (|.g2.| + r) by A10;
|.(((seq (#) seq9) . m) - g).| = |.((((seq . m) * (seq9 . m)) - (((seq . m) * g2) - ((seq . m) * g2))) - (g1 * g2)).| by SEQ_1:8
.= |.(((seq . m) * ((seq9 . m) - g2)) + (((seq . m) - g1) * g2)).| ;
then A17: |.(((seq (#) seq9) . m) - g).| <= |.((seq . m) * ((seq9 . m) - g2)).| + |.(((seq . m) - g1) * g2).| by COMPLEX1:56;
|.(seq . m).| < r by A6;
then |.(seq . m).| * |.((seq9 . m) - g2).| < r * (p / (|.g2.| + r)) by A13, A14, A15, XREAL_1:96;
then A18: |.((seq . m) * ((seq9 . m) - g2)).| < r * (p / (|.g2.| + r)) by COMPLEX1:65;
|.(((seq . m) - g1) * g2).| = |.g2.| * |.((seq . m) - g1).| by COMPLEX1:65;
then A19: |.(((seq . m) - g1) * g2).| <= |.g2.| * (p / (|.g2.| + r)) by A7, A16, XREAL_1:64;
(r * (p / (|.g2.| + r))) + (|.g2.| * (p / (|.g2.| + r))) = (p / (|.g2.| + r)) * (|.g2.| + r)
.= p by A8, XCMPLX_1:87 ;
then |.((seq . m) * ((seq9 . m) - g2)).| + |.(((seq . m) - g1) * g2).| < p by A18, A19, XREAL_1:8;
hence |.(((seq (#) seq9) . m) - g).| < p by A17, XXREAL_0:2; :: thesis: verum