theorem Th28: :: COMPLSP2:34

for x being complex-valued FinSequence holds x + (- x) = 0c (len x)