let c, c1 be complex number ; :: 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:66
.= multcomplex . a,s by FUNCT_1:35
.= c * c1 by BINOP_2:def 5 ; :: thesis: verum