theorem Th4: :: BHSP_2:4

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