let n be Element of NAT ; :: thesis: for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
let c1, c2 be Element of COMPLEX ; :: thesis: for z being Element of COMPLEX n holds c1 * (c2 * z) = (c1 * c2) * z
let z be Element of COMPLEX n; :: thesis: c1 * (c2 * z) = (c1 * c2) * z
thus (c1 * c2) * z = (multcomplex [;] (multcomplex . c1,c2),(id COMPLEX )) * z by BINOP_2:def 5
.= (multcomplex [;] c1,(multcomplex [;] c2,(id COMPLEX ))) * z by FUNCOP_1:77
.= ((multcomplex [;] c1,(id COMPLEX )) * (multcomplex [;] c2,(id COMPLEX ))) * z by FUNCOP_1:69
.= c1 * (c2 * z) by RELAT_1:55 ; :: thesis: verum