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
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence st Cseq is convergent & seq is convergent holds
Cseq * seq is convergent
let Cseq be Complex_Sequence; :: thesis: ( Cseq is convergent & seq is convergent implies Cseq * seq is convergent )
assume that
A1: Cseq is convergent and
A2: seq is convergent ; :: thesis: Cseq * seq is convergent
consider p being Complex such that
A3: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
|.((Cseq . n) - p).| < r by A1, COMSEQ_2:def 4;
consider g being Point of X such that
A4: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.((seq . n) - g).|| < r by A2, CLVECT_2:9;

now

take h = p * g; :: thesis: for r being Real st r > 0 holds
ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
Cseq is bounded by A1, Lm1;
then consider b being Real such that
A5: b > 0 and
A6: for n being Element of NAT holds |.(Cseq . n).| < b by COMSEQ_2:8;
A7: ||.g.|| >= 0 by CSSPACE:46;
A8: b + ||.g.|| > 0 + 0 by A5, CSSPACE:46, XREAL_1:10;
let r be Real; :: thesis: ( r > 0 implies ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r )
assume r > 0 ; :: thesis: ex m being Element of NAT st
for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
then A9: r / (b + ||.g.||) > 0 by A8, XREAL_1:141;
then consider m1 being Element of NAT such that
A10: for n being Element of NAT st n >= m1 holds
|.((Cseq . n) - p).| < r / (b + ||.g.||) by A3;
consider m2 being Element of NAT such that
A11: for n being Element of NAT st n >= m2 holds
||.((seq . n) - g).|| < r / (b + ||.g.||) by A4, A9;
take m = m1 + m2; :: thesis: for n being Element of NAT st n >= m holds
||.(((Cseq * seq) . n) - h).|| < r
let n be Element of NAT ; :: thesis: ( n >= m implies ||.(((Cseq * seq) . n) - h).|| < r )
assume A12: n >= m ; :: thesis: ||.(((Cseq * seq) . n) - h).|| < r
m1 + m2 >= m1 by NAT_1:12;
then n >= m1 by A12, XXREAL_0:2;
then A13: |.((Cseq . n) - p).| <= r / (b + ||.g.||) by A10;
A14: |.(Cseq . n).| < b by A6;
m >= m2 by NAT_1:12;
then n >= m2 by A12, XXREAL_0:2;
then A15: ||.((seq . n) - g).|| < r / (b + ||.g.||) by A11;
||.(((Cseq * seq) . n) - (p * g)).|| = ||.(((Cseq . n) * (seq . n)) - (p * g)).|| by Def9
.= ||.((((Cseq . n) * (seq . n)) - (p * g)) + H₁(X)).|| by RLVECT_1:10
.= ||.((((Cseq . n) * (seq . n)) - (p * g)) + (((Cseq . n) * g) - ((Cseq . n) * g))).|| by RLVECT_1:28
.= ||.(((Cseq . n) * (seq . n)) - ((p * g) - (((Cseq . n) * g) - ((Cseq . n) * g)))).|| by RLVECT_1:43
.= ||.(((Cseq . n) * (seq . n)) - (((Cseq . n) * g) + ((p * g) - ((Cseq . n) * g)))).|| by RLVECT_1:43
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) - ((p * g) - ((Cseq . n) * g))).|| by RLVECT_1:41
.= ||.((((Cseq . n) * (seq . n)) - ((Cseq . n) * g)) + (((Cseq . n) * g) - (p * g))).|| by RLVECT_1:47 ;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.(((Cseq . n) * (seq . n)) - ((Cseq . n) * g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CSSPACE:48;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) * g) - (p * g)).|| by CLVECT_1:10;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= ||.((Cseq . n) * ((seq . n) - g)).|| + ||.(((Cseq . n) - p) * g).|| by CLVECT_1:11;
then ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + ||.(((Cseq . n) - p) * g).|| by CSSPACE:45;
then A16: ||.(((Cseq * seq) . n) - (p * g)).|| <= (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) by CSSPACE:45;
A17: |.(Cseq . n).| >= 0 by COMPLEX1:132;
||.((seq . n) - g).|| >= 0 by CSSPACE:46;
then A18: |.(Cseq . n).| * ||.((seq . n) - g).|| < b * (r / (b + ||.g.||)) by A14, A15, A17, XREAL_1:98;
||.g.|| * |.((Cseq . n) - p).| <= ||.g.|| * (r / (b + ||.g.||)) by A7, A13, XREAL_1:66;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < (b * (r / (b + ||.g.||))) + (||.g.|| * (r / (b + ||.g.||))) by A18, XREAL_1:10;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + (||.g.|| * (r / (b + ||.g.||))) by XCMPLX_1:75;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) / (b + ||.g.||)) + ((||.g.|| * r) / (b + ||.g.||)) by XCMPLX_1:75;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b * r) + (||.g.|| * r)) / (b + ||.g.||) by XCMPLX_1:63;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < ((b + ||.g.||) * r) / (b + ||.g.||) ;
then (|.(Cseq . n).| * ||.((seq . n) - g).||) + (||.g.|| * |.((Cseq . n) - p).|) < r by A8, XCMPLX_1:90;
hence ||.(((Cseq * seq) . n) - h).|| < r by A16, XXREAL_0:2; :: thesis: verum

end;

hence Cseq * seq is convergent by CLVECT_2:9; :: thesis: verum