let Rseq be Real_Sequence; :: thesis: for X being RealUnitarySpace
for seq being sequence of X st X is Hilbert & seq is Cauchy & Rseq is Cauchy holds
Rseq * seq is Cauchy
let X be RealUnitarySpace; :: thesis: for seq being sequence of X st X is Hilbert & seq is Cauchy & Rseq is Cauchy holds
Rseq * seq is Cauchy
let seq be sequence of X; :: thesis: ( X is Hilbert & seq is Cauchy & Rseq is Cauchy implies Rseq * seq is Cauchy )
assume that
A1: X is Hilbert and
A2: seq is Cauchy and
A3: 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 A4: 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
A5: for n, m being Element of NAT st n >= k & m >= k holds
abs ((Rseq . n) - (Rseq . m)) < r by A3, A4, 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 A5; :: thesis: verum

end;

then A6: Rseq is convergent by SEQ_4:58;
X is complete by A1, BHSP_3:def 7;
then seq is convergent by A2, BHSP_3:def 6;
hence Rseq * seq is Cauchy by A6, Th50, BHSP_3:9; :: thesis: verum