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