let X be ComplexUnitarySpace; :: thesis: for seq being sequence of X
for Cseq being Complex_Sequence st X is Hilbert & seq is Cauchy & Cseq is Cauchy holds
Cseq * seq is Cauchy
let seq be sequence of X; :: thesis: for Cseq being Complex_Sequence st X is Hilbert & seq is Cauchy & Cseq is Cauchy holds
Cseq * seq is Cauchy
let Cseq be Complex_Sequence; :: thesis: ( X is Hilbert & seq is Cauchy & Cseq is Cauchy implies Cseq * seq is Cauchy )
assume that
A1: X is Hilbert and
A2: seq is Cauchy and
A3: Cseq is Cauchy ; :: thesis: Cseq * seq is Cauchy

now

let r be Real; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r )
assume r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r
then consider k being Element of NAT such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
|.((Cseq . n) - (Cseq . m)).| < r by A3, Def10;
take k = k; :: thesis: for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r
thus for n being Element of NAT st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r by A4; :: thesis: verum

end;

then A5: Cseq is convergent by COMSEQ_3:46;
X is complete by A1, CLVECT_2:def 13;
then seq is convergent by A2, CLVECT_2:def 12;
hence Cseq * seq is Cauchy by A5, Th48, CLVECT_2:65; :: thesis: verum