theorem :: CLVECT_3:47

for X being ComplexUnitarySpace
for seq being sequence of X
for Cseq being Complex_Sequence holds Cseq * (- seq) = (- Cseq) * seq