let n be 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:62
.= ((multcomplex [;] (c1,(id COMPLEX))) * (multcomplex [;] (c2,(id COMPLEX)))) * z by FUNCOP_1:55
.= c1 * (c2 * z) by RELAT_1:36 ; :: thesis: verum