let n be Nat; :: thesis: 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 ; :: thesis: for z being Element of COMPLEX n holds (c1 + c2) * z = (c1 * z) + (c2 * z)
let z be Element of COMPLEX n; :: thesis: (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 ; :: thesis: verum