theorem :: BHSP_1:50
for X being RealUnitarySpace
for seq being sequence of X holds seq = seq + (0. X)