let z be FinSequence of COMPLEX ; :: thesis: for a, b being Complex holds a * (b * z) = (a * b) * z
let a, b be Complex; :: thesis: a * (b * z) = (a * b) * z
reconsider aa = a, bb = b, ab = a * b as Element of COMPLEX by XCMPLX_0:def 2;
thus (a * b) * z = (multcomplex [;] (ab,(id COMPLEX))) * z by Lm1
.= (multcomplex [;] ((multcomplex . (aa,bb)),(id COMPLEX))) * z by BINOP_2:def 5
.= (multcomplex [;] (aa,(multcomplex [;] (bb,(id COMPLEX))))) * z by FUNCOP_1:62
.= ((multcomplex [;] (aa,(id COMPLEX))) * (multcomplex [;] (bb,(id COMPLEX)))) * z by FUNCOP_1:55
.= (multcomplex [;] (aa,(id COMPLEX))) * ((multcomplex [;] (bb,(id COMPLEX))) * z) by RELAT_1:36
.= (multcomplex [;] (aa,(id COMPLEX))) * (b * z) by Lm1
.= a * (b * z) by Lm1 ; :: thesis: verum