let z be FinSequence of COMPLEX ; :: thesis: for a, b being complex number holds (a - b) * z = (a * z) - (b * z)
let a, b be complex number ; :: 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 Th63
.= (a * z) - (b * z) by Th54 ;
hence (a - b) * z = (a * z) - (b * z) ; :: thesis: verum