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

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