let a, b be complex number ; :: thesis: multcomplex . a,b = a * b
reconsider a' = a, b' = b as Element of COMPLEX by XCMPLX_0:def 2;
multcomplex . a',b' = a' * b' by BINOP_2:def 5;
hence multcomplex . a,b = a * b ; :: thesis: verum