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