theorem :: CSSPACE:65

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