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 as Element of COMPLEX by XCMPLX_0:def 2;
(a - b) * z = (a + (- b)) * z
.= (aa * z) + ((- bb) * z) by Th52
.= (a * z) - (b * z) by Th45 ;
hence (a - b) * z = (a * z) - (b * z) ; :: thesis: verum