now :: thesis: for c1, c2, c3 being Element of COMPLEX holds
( multcomplex . (c1,(addcomplex . (c2,c3))) = addcomplex . ((multcomplex . (c1,c2)),(multcomplex . (c1,c3))) & multcomplex . ((addcomplex . (c1,c2)),c3) = addcomplex . ((multcomplex . (c1,c3)),(multcomplex . (c2,c3))) )

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:11; :: thesis: verum