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