let seq, seq9 be Real_Sequence; ( 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
; 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 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))).| < plet p be
Real;
( 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
;
ex n being set st
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < pthen 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;
for m being Nat st n <= m holds
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < plet m be
Nat;
( n <= m implies |.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < p )assume A10:
n <= m
;
|.(((seq (#) seq9) . m) - ((lim seq) * (lim seq9))).| < pA11:
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;
verum end;
hence
lim (seq (#) seq9) = (lim seq) * (lim seq9)
by A1, A2, Def6; verum