theorem :: CSSPACE:73

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