let c1, c2 be Complex; :: thesis: <*c1*> - <*c2*> = <*(c1 - c2)*>
reconsider s1 = c1, s2 = c2 as Element of COMPLEX by XCMPLX_0:def 2;
<*s1*> - <*s2*> = <*(diffcomplex . (s1,s2))*> by FINSEQ_2:74
.= <*(c1 - c2)*> by BINOP_2:def 4 ;
hence <*c1*> - <*c2*> = <*(c1 - c2)*> ; :: thesis: verum