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

now

let r be real number ; :: thesis: ( r > 0 implies ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r )
assume A3: r > 0 ; :: thesis: ex k being Element of NAT st
for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r
r is Real by XREAL_0:def 1;
then consider k being Element of NAT such that
A4: for n, m being Element of NAT st n >= k & m >= k holds
abs ((Rseq . n) - (Rseq . m)) < r by A2, A3, Def10;
take k = k; :: thesis: for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r
thus for n being Element of NAT st n >= k holds
abs ((Rseq . n) - (Rseq . k)) < r by A4; :: thesis: verum

end;

then A5: Rseq is convergent by SEQ_4:41;
seq is convergent by A1, BHSP_3:def 4;
hence Rseq * seq is Cauchy by A5, Th50, BHSP_3:9; :: thesis: verum