theorem Th48: :: BHSP_4:48

for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X st Rseq is convergent & seq is convergent holds
Rseq * seq is convergent