now

let c1, c2, c3 be Element of COMPLEX ; :: thesis: ( multcomplex . c1,(addcomplex . c2,c3) = addcomplex . (multcomplex . c1,c2),(multcomplex . c1,c3) & multcomplex . (addcomplex . c1,c2),c3 = addcomplex . (multcomplex . c1,c3),(multcomplex . c2,c3) )
thus multcomplex . c1,(addcomplex . c2,c3) = multcomplex . c1,(c2 + c3) by BINOP_2:def 3
.= c1 * (c2 + c3) by BINOP_2:def 5
.= (c1 * c2) + (c1 * c3)
.= addcomplex . (c1 * c2),(c1 * c3) by BINOP_2:def 3
.= addcomplex . (multcomplex . c1,c2),(c1 * c3) by BINOP_2:def 5
.= addcomplex . (multcomplex . c1,c2),(multcomplex . c1,c3) by BINOP_2:def 5 ; :: thesis: multcomplex . (addcomplex . c1,c2),c3 = addcomplex . (multcomplex . c1,c3),(multcomplex . c2,c3)
thus multcomplex . (addcomplex . c1,c2),c3 = multcomplex . (c1 + c2),c3 by BINOP_2:def 3
.= (c1 + c2) * c3 by BINOP_2:def 5
.= (c1 * c3) + (c2 * c3)
.= addcomplex . (c1 * c3),(c2 * c3) by BINOP_2:def 3
.= addcomplex . (multcomplex . c1,c3),(c2 * c3) by BINOP_2:def 5
.= addcomplex . (multcomplex . c1,c3),(multcomplex . c2,c3) by BINOP_2:def 5 ; :: thesis: verum

end;

hence multcomplex is_distributive_wrt addcomplex by BINOP_1:23; :: thesis: verum