for Cseq being Complex_Sequence
for X being ComplexHilbertSpace
for seq being sequence of X st seq is Cauchy & Cseq is Cauchy holds
Cseq * seq is Cauchy