for S being RealNormSpace
for seq being sequence of S holds - seq = (- 1) * seq