let X be ComplexUnitarySpace; for seq being sequence of X
for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
let seq be sequence of X; for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
let Cseq be Complex_Sequence; ( Cseq is convergent & seq is convergent implies ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) ) )
assume that
A1:
Cseq is convergent
and
A2:
seq is convergent
; ( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
Cseq is bounded
by A1;
then consider b being Real such that
A3:
b > 0
and
A4:
for n being Nat holds |.(Cseq . n).| < b
by COMSEQ_2:8;
A5:
b + ||.(lim seq).|| > 0 + 0
by A3, CSSPACE:44, XREAL_1:8;
A6:
||.(lim seq).|| >= 0
by CSSPACE:44;
A7:
now for r being Real st r > 0 holds
ex m being set st
for n being Nat st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < rlet r be
Real;
( r > 0 implies ex m being set st
for n being Nat st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r )assume
r > 0
;
ex m being set st
for n being Nat st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < rthen A8:
r / (b + ||.(lim seq).||) > 0
by A5;
then consider m1 being
Nat such that A9:
for
n being
Nat st
n >= m1 holds
|.((Cseq . n) - (lim Cseq)).| < r / (b + ||.(lim seq).||)
by A1, COMSEQ_2:def 6;
consider m2 being
Nat such that A10:
for
n being
Nat st
n >= m2 holds
dist (
(seq . n),
(lim seq))
< r / (b + ||.(lim seq).||)
by A2, A8, CLVECT_2:def 2;
take m =
m1 + m2;
for n being Nat st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < rlet n be
Nat;
( n >= m implies dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r )assume A11:
n >= m
;
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r
m1 + m2 >= m1
by NAT_1:12;
then
n >= m1
by A11, XXREAL_0:2;
then
|.((Cseq . n) - (lim Cseq)).| <= r / (b + ||.(lim seq).||)
by A9;
then A12:
||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).| <= ||.(lim seq).|| * (r / (b + ||.(lim seq).||))
by A6, XREAL_1:64;
A13:
||.((seq . n) - (lim seq)).|| >= 0
by CSSPACE:44;
m >= m2
by NAT_1:12;
then
n >= m2
by A11, XXREAL_0:2;
then
dist (
(seq . n),
(lim seq))
< r / (b + ||.(lim seq).||)
by A10;
then A14:
||.((seq . n) - (lim seq)).|| < r / (b + ||.(lim seq).||)
by CSSPACE:def 16;
(
|.(Cseq . n).| < b &
|.(Cseq . n).| >= 0 )
by A4, COMPLEX1:46;
then
|.(Cseq . n).| * ||.((seq . n) - (lim seq)).|| < b * (r / (b + ||.(lim seq).||))
by A14, A13, XREAL_1:96;
then
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < (b * (r / (b + ||.(lim seq).||))) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||)))
by A12, XREAL_1:8;
then
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + (||.(lim seq).|| * (r / (b + ||.(lim seq).||)))
by XCMPLX_1:74;
then
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) / (b + ||.(lim seq).||)) + ((||.(lim seq).|| * r) / (b + ||.(lim seq).||))
by XCMPLX_1:74;
then
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b * r) + (||.(lim seq).|| * r)) / (b + ||.(lim seq).||)
by XCMPLX_1:62;
then
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < ((b + ||.(lim seq).||) * r) / (b + ||.(lim seq).||)
;
then A15:
(|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|) < r
by A5, XCMPLX_1:89;
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| =
||.(((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))).||
by Def8
.=
||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + H1(X)).||
by RLVECT_1:4
.=
||.((((Cseq . n) * (seq . n)) - ((lim Cseq) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq)))).||
by RLVECT_1:15
.=
||.(((Cseq . n) * (seq . n)) - (((lim Cseq) * (lim seq)) - (((Cseq . n) * (lim seq)) - ((Cseq . n) * (lim seq))))).||
by RLVECT_1:29
.=
||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * (lim seq)) + (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq))))).||
by RLVECT_1:29
.=
||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) - (((lim Cseq) * (lim seq)) - ((Cseq . n) * (lim seq)))).||
by RLVECT_1:27
.=
||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))) + (((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq)))).||
by RLVECT_1:33
;
then
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).||
by CSSPACE:46;
then
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) * (lim seq)) - ((lim Cseq) * (lim seq))).||
by CLVECT_1:9;
then
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= ||.((Cseq . n) * ((seq . n) - (lim seq))).|| + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).||
by CLVECT_1:10;
then
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + ||.(((Cseq . n) - (lim Cseq)) * (lim seq)).||
by CSSPACE:43;
then
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| <= (|.(Cseq . n).| * ||.((seq . n) - (lim seq)).||) + (||.(lim seq).|| * |.((Cseq . n) - (lim Cseq)).|)
by CSSPACE:43;
then
||.(((Cseq * seq) . n) - ((lim Cseq) * (lim seq))).|| < r
by A15, XXREAL_0:2;
hence
dist (
((Cseq * seq) . n),
((lim Cseq) * (lim seq)))
< r
by CSSPACE:def 16;
verum end;
Cseq * seq is convergent
by A1, A2, Th48;
hence
( Cseq * seq is convergent & lim (Cseq * seq) = (lim Cseq) * (lim seq) )
by A7, CLVECT_2:def 2; verum