theorem :: SEQ_1:17

for seq being Real_Sequence holds - seq = (- 1) (#) seq ;