let z be FinSequence of COMPLEX ; :: thesis: for a, b being Complex holds (a + b) * z = (a * z) + (b * z)
let a, b be Complex; :: thesis: (a + b) * z = (a * z) + (b * z)
reconsider aa = a, bb = b, ab = a + 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 [;] (ab,(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 FINSEQOP:35, SEQ_4:54
.= addcomplex .: (((multcomplex [;] (aa,(id COMPLEX))) * z),((multcomplex [;] (bb,(id COMPLEX))) * z)) by FUNCOP_1:25
.= ((multcomplex [;] (aa,(id COMPLEX))) * z) + ((multcomplex [;] (bb,(id COMPLEX))) * z) by SEQ_4:def 6
.= (a * z) + ((multcomplex [;] (bb,(id COMPLEX))) * z) by Lm1
.= (a * z) + (b * z) by Lm1 ; :: thesis: verum