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