theorem :: COMPLSP2:23

for z being FinSequence of COMPLEX holds (- z) *' = - (z *')