theorem Th9: :: COMPLSP2:13

for i being Element of NAT
for x being FinSequence of COMPLEX holds (- x) . i = - (x . i)