theorem Th11: :: TOPRNS_1:11

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