let c be complex number ; :: thesis: for x, y being FinSequence of COMPLEX st len x = len y holds
c * (x - y) = (c * x) - (c * y)
let x, y be FinSequence of COMPLEX ; :: thesis: ( len x = len y implies c * (x - y) = (c * x) - (c * y) )
assume A1: len x = len y ; :: thesis: c * (x - y) = (c * x) - (c * y)
reconsider cc = c as Element of COMPLEX by XCMPLX_0:def 2;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:110;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
set cM = cc multcomplex ;
c * (x - y) = (cc multcomplex) * (x + (- y)) by SEQ_4:def 12
.= (cc multcomplex) * (addcomplex .: (x,(- y))) by SEQ_4:def 9
.= addcomplex .: (((cc multcomplex) * x9),((cc multcomplex) * (- y9))) by A1, FINSEQOP:52, SEQ_4:73
.= ((cc multcomplex) * x) + ((cc multcomplex) * (- y)) by SEQ_4:def 9
.= (c * x) + ((cc multcomplex) * (- y)) by SEQ_4:def 12
.= (c * x) + (c * (- y)) by SEQ_4:def 12
.= (c * x) - (c * y) by Th42 ;
hence c * (x - y) = (c * x) - (c * y) ; :: thesis: verum