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