theorem Th16: :: SEQM_3:16

for k being Nat
for seq being Real_Sequence holds (- seq) ^\ k = - (seq ^\ k)