let z be FinSequence of COMPLEX ; :: thesis: for a, b being complex number holds (a + b) * z = (a * z) + (b * z)
let a, b be complex number ; :: thesis: (a + b) * z = (a * z) + (b * z)
reconsider aa = a, bb = b as Element of COMPLEX by XCMPLX_0:def 2;
set c1M = multcomplex [;] aa,(id COMPLEX );
set c2M = multcomplex [;] bb,(id COMPLEX );
thus (a + b) * z = (multcomplex [;] (aa + bb),(id COMPLEX )) * z by Lm1
.= (multcomplex [;] (addcomplex . aa,bb),(id COMPLEX )) * z by BINOP_2:def 3
.= (addcomplex .: (multcomplex [;] aa,(id COMPLEX )),(multcomplex [;] bb,(id COMPLEX ))) * z by COMPLSP1:15, FINSEQOP:36
.= addcomplex .: ((multcomplex [;] aa,(id COMPLEX )) * z),((multcomplex [;] bb,(id COMPLEX )) * z) by FUNCOP_1:31
.= ((multcomplex [;] aa,(id COMPLEX )) * z) + ((multcomplex [;] bb,(id COMPLEX )) * z) by COMPLSP1:def 7
.= (a * z) + ((multcomplex [;] bb,(id COMPLEX )) * z) by Lm1
.= (a * z) + (b * z) by Lm1 ; :: thesis: verum