theorem :: RVSUM_2:50

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