let X be ComplexUnitarySpace; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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 :: thesis: 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))) < r

let r be Real; :: thesis: ( 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 ; :: thesis: ex m being set st
for n being Nat st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r
then 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; :: thesis: for n being Nat st n >= m holds
dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r
let n be Nat; :: thesis: ( n >= m implies dist (((Cseq * seq) . n),((lim Cseq) * (lim seq))) < r )
assume A11: n >= m ; :: thesis: 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))) + H₁(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; :: thesis: 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; :: thesis: verum