theorem Th5: :: COMPLSP2:5

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