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