let c1, c2 be Complex; :: thesis: Product <%c1,c2%> = c1 * c2
( c1 in COMPLEX & c2 in COMPLEX ) by XCMPLX_0:def 2;
then multcomplex "**" <%c1,c2%> = multcomplex . (c1,c2) by AFINSQ_2:38
.= c1 * c2 by BINOP_2:def 5 ;
hence Product <%c1,c2%> = c1 * c2 ; :: thesis: verum