theorem :: BHSP_1:58

for X being RealUnitarySpace
for seq being sequence of X holds seq = seq - (0. X)