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