for CNS being ComplexNormSpace
for seq being sequence of CNS holds - seq = (- 1r) * seq