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