let n be Element of 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 Th15, FINSEQOP:36
.= (c1 * z) + (c2 * z) by FUNCOP_1:31 ; :: thesis: verum