let z be FinSequence of COMPLEX ; :: thesis: for a, b being complex number holds a * (b * z) = (a * b) * z
let a, b be complex number ; :: thesis: a * (b * z) = (a * b) * z
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def 2;
thus (a * b) * z = (multcomplex [;] (aa * bb),(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:77
.= ((multcomplex [;] aa,(id COMPLEX )) * (multcomplex [;] bb,(id COMPLEX ))) * z by FUNCOP_1:69
.= (multcomplex [;] aa,(id COMPLEX )) * ((multcomplex [;] bb,(id COMPLEX )) * z) by RELAT_1:55
.= (multcomplex [;] aa,(id COMPLEX )) * (b * z) by Lm1
.= a * (b * z) by Lm1 ; :: thesis: verum