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