theorem Th14: :: BHSP_3:33

for X being RealUnitarySpace
for seq being sequence of X
for k being Nat holds (- seq) ^\ k = - (seq ^\ k)