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:53
.= multcomplex . (a,b)
.= a * b by BINOP_2:def 5 ; :: thesis: verum