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*> = <*(addcomplex . (s1,s2))*> by FINSEQ_2:74
.= <*(c1 + c2)*> by BINOP_2:def 3 ;
hence <*c1*> + <*c2*> = <*(c1 + c2)*> ; :: thesis: verum