theorem :: MATRIXC1:45

for F being FinSequence of COMPLEX holds Sum (- F) = - (Sum F)