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

now :: thesis: for r being Real st r > 0 holds
ex k being Nat st
for n being Nat st n >= k holds
|.((Cseq . n) - (Cseq . k)).| < r

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

end;

then A4: Cseq is convergent by COMSEQ_3:46;
seq is convergent by A1, CLVECT_2:def 11;
hence Cseq * seq is Cauchy by A4, Th48, CLVECT_2:65; :: thesis: verum