theorem :: CSSPACE:69

for X being ComplexUnitarySpace
for seq being sequence of X holds 1r * seq = seq