let n be Nat; for c1, c2 being Element of COMPLEX
for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
let c1, c2 be Element of COMPLEX ; for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
let z be Element of COMPLEX n; (c1 + c2) * z = (c1 * z) + (c2 * z)
set c1M = multcomplex [;] (c1,(id COMPLEX));
set c2M = multcomplex [;] (c2,(id COMPLEX));
thus (c1 + c2) * z =
(multcomplex [;] ((addcomplex . (c1,c2)),(id COMPLEX))) * z
by BINOP_2:def 3
.=
(addcomplex .: ((multcomplex [;] (c1,(id COMPLEX))),(multcomplex [;] (c2,(id COMPLEX))))) * z
by Th54, FINSEQOP:35
.=
(c1 * z) + (c2 * z)
by FUNCOP_1:25
; verum