let z be FinSequence of COMPLEX ; for a, b being Complex holds a * (b * z) = (a * b) * z
let a, b be Complex; 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
; verum