let c be Complex; :: thesis: - <*c*> = <*(- c)*>
reconsider s = c as Element of COMPLEX by XCMPLX_0:def 2;
- <*s*> = <*(compcomplex . s)*> by FINSEQ_2:35
.= <*(- c)*> by BINOP_2:def 1 ;
hence - <*c*> = <*(- c)*> ; :: thesis: verum