let z be FinSequence of COMPLEX ; :: thesis: (- z) *' = - (z *')
(- z) *' = ((- 1r) *') * (z *') by Th17, COMPLEX1:def 4
.= - (z *') by COMPLEX1:30, COMPLEX1:33, COMPLEX1:def 4 ;
hence (- z) *' = - (z *') ; :: thesis: verum