let seq, seq9 be Real_Sequence; :: thesis: ( seq is convergent & seq9 is convergent implies lim (seq (#) seq9) = (lim seq) * (lim seq9) )
assume that
A1: seq is convergent and
A2: seq9 is convergent ; :: thesis: lim (seq (#) seq9) = (lim seq) * (lim seq9)
consider r being Real such that
A3: 0 < r and
A4: for n being Nat holds |.(seq . n).| < r by A1, Th3;
A5: 0 <= |.(lim seq9).| by COMPLEX1:46;
A6: 0 + 0 < |.(lim seq9).| + r by A3, COMPLEX1:46, XREAL_1:8;

now :: thesis: for p being Real st 0 < p holds
ex n being set st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p

let p be Real; :: thesis: ( 0 < p implies ex n being set st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p )
assume 0 < p ; :: thesis: ex n being set st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p
then A7: 0 < p / (|.(lim seq9).| + r) by A6;
then consider n1 being Nat such that
A8: for m being Nat st n1 <= m holds
|.((seq . m) - (lim seq)).| < p / (|.(lim seq9).| + r) by A1, Def6;
consider n2 being Nat such that
A9: for m being Nat st n2 <= m holds
|.((seq9 . m) - (lim seq9)).| < p / (|.(lim seq9).| + r) by A2, A7, Def6;
take n = n1 + n2; :: thesis: for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p
let m be Nat; :: thesis: ( n <= m implies |.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p )
assume A10: n <= m ; :: thesis: |.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p
A11: 0 <= |.(seq . m).| by COMPLEX1:46;
A12: 0 <= |.((seq9 . m) - (lim seq9)).| by COMPLEX1:46;
n2 <= n by NAT_1:12;
then n2 <= m by A10, XXREAL_0:2;
then A13: |.((seq9 . m) - (lim seq9)).| < p / (|.(lim seq9).| + r) by A9;
n1 <= n1 + n2 by NAT_1:12;
then n1 <= m by A10, XXREAL_0:2;
then A14: |.((seq . m) - (lim seq)).| <= p / (|.(lim seq9).| + r) by A8;
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| = |.((((seq . m) * (seq9 . m)) - (((seq . m) * (lim seq9)) - ((seq . m) * (lim seq9)))) - ((lim seq) * (lim seq9))).| by SEQ_1:8
.= |.(((seq . m) * ((seq9 . m) - (lim seq9))) + (((seq . m) - (lim seq)) * (lim seq9))).| ;
then A15: |.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| <= |.((seq . m) * ((seq9 . m) - (lim seq9))).| + |.(((seq . m) - (lim seq)) * (lim seq9)).| by COMPLEX1:56;
|.(seq . m).| < r by A4;
then |.(seq . m).| * |.((seq9 . m) - (lim seq9)).| < r * (p / (|.(lim seq9).| + r)) by A11, A12, A13, XREAL_1:96;
then A16: |.((seq . m) * ((seq9 . m) - (lim seq9))).| < r * (p / (|.(lim seq9).| + r)) by COMPLEX1:65;
|.(((seq . m) - (lim seq)) * (lim seq9)).| = |.(lim seq9).| * |.((seq . m) - (lim seq)).| by COMPLEX1:65;
then A17: |.(((seq . m) - (lim seq)) * (lim seq9)).| <= |.(lim seq9).| * (p / (|.(lim seq9).| + r)) by A5, A14, XREAL_1:64;
(r * (p / (|.(lim seq9).| + r))) + (|.(lim seq9).| * (p / (|.(lim seq9).| + r))) = (p / (|.(lim seq9).| + r)) * (|.(lim seq9).| + r)
.= p by A6, XCMPLX_1:87 ;
then |.((seq . m) * ((seq9 . m) - (lim seq9))).| + |.(((seq . m) - (lim seq)) * (lim seq9)).| < p by A16, A17, XREAL_1:8;
hence |.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p by A15, XXREAL_0:2; :: thesis: verum

end;

hence lim (seq (#) seq9) = (lim seq) * (lim seq9) by A1, A2, Def6; :: thesis: verum