reconsider a' = a, b' = b as Element of COMPLEX by XCMPLX_0:def 2;
assume ( x = a & y = b ) ; :: thesis: x * y = a * b
hence x * y = multcomplex . a',b' by Def1
.= a * b by BINOP_2:def 5 ;
:: thesis: verum