let c1, c2 be complex number ; :: 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:88
.= <*(c1 * c2)*> by BINOP_2:def 5 ;
hence mlt <*c1*>,<*c2*> = <*(c1 * c2)*> ; :: thesis: verum