for seq being Real_Sequence holds (- seq) " = (- 1) (#) (seq ") by Lm1, Th44;