reconsider c9 = c as Element of COMPLEX by XCMPLX_0:def 2;
multcomplex [;] (c9,(id COMPLEX)) is UnOp of COMPLEX ;
hence multcomplex [;] (c,(id COMPLEX)) is UnOp of COMPLEX ; :: thesis: verum