for Rseq being Real_Sequence
for X being RealUnitarySpace
for seq being sequence of X holds Rseq * (- seq) = (- Rseq) * seq