theorem Th3: :: BHSP_2:3

for X being RealUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent