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