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 COMPLSP1:def 10
.= (cc multcomplex ) * (addcomplex .: x,(- y)) by COMPLSP1:def 7
.= addcomplex .: ((cc multcomplex ) * x9),((cc multcomplex ) * (- y9)) by A1, COMPLSP1:17, FINSEQOP:52
.= ((cc multcomplex ) * x) + ((cc multcomplex ) * (- y)) by COMPLSP1:def 7
.= (c * x) + ((cc multcomplex ) * (- y)) by COMPLSP1:def 10
.= (c * x) + (c * (- y)) by COMPLSP1:def 10
.= (c * x) - (c * y) by Th42 ;
hence c * (x - y) = (c * x) - (c * y) ; :: thesis: verum