let c, c9 be Element of COMPLEX ; :: thesis: (multcomplex [;] (c,(id COMPLEX))) . c9 = c * c9
thus (multcomplex [;] (c,(id COMPLEX))) . c9 = multcomplex . (c,((id COMPLEX) . c9)) by FUNCOP_1:66
.= multcomplex . (c,c9) by FUNCT_1:35
.= c * c9 by BINOP_2:def 5 ; :: thesis: verum