theorem :: BHSP_3:37

for X being RealUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent