theorem Th87: :: CLVECT_2:87

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