let c, c1 be Complex; :: thesis: (multcomplex [;] (c,(id COMPLEX))) . c1 = c * c1
reconsider a = c, s = c1 as Element of COMPLEX by XCMPLX_0:def 2;
thus (multcomplex [;] (c,(id COMPLEX))) . c1 = multcomplex . (a,((id COMPLEX) . s)) by FUNCOP_1:53
.= multcomplex . (a,s)
.= c * c1 by BINOP_2:def 5 ; :: thesis: verum