let c be Complex; :: 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)
set cM = c multcomplex ;
reconsider y9 = y as Element of (len y) -tuples_on COMPLEX by FINSEQ_2:92;
reconsider x9 = x as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:92;
A2: c is Element of COMPLEX by XCMPLX_0:def 2;
c * (x + y) = (c multcomplex) * (x + y) by SEQ_4:def 9
.= (c multcomplex) * (addcomplex .: (x,y)) by SEQ_4:def 6
.= addcomplex .: (((c multcomplex) * x9),((c multcomplex) * y9)) by A1, A2, FINSEQOP:51, SEQ_4:56
.= ((c multcomplex) * x) + ((c multcomplex) * y) by SEQ_4:def 6
.= (c * x) + ((c multcomplex) * y) by SEQ_4:def 9
.= (c * x) + (c * y) by SEQ_4:def 9 ;
hence c * (x + y) = (c * x) + (c * y) ; :: thesis: verum