theorem Th17: :: TOPRNS_1:17

for N being Nat
for seq being Real_Sequence of N holds - (- seq) = seq