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