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)
set cM = c multcomplex ;
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;
A2: c is Element of COMPLEX by XCMPLX_0:def 2;
c * (x + y) = (c multcomplex ) * (x + y) by COMPLSP1:def 10
.= (c multcomplex ) * (addcomplex .: x,y) by COMPLSP1:def 7
.= addcomplex .: ((c multcomplex ) * x9),((c multcomplex ) * y9) by A1, A2, COMPLSP1:17, FINSEQOP:52
.= ((c multcomplex ) * x) + ((c multcomplex ) * y) by COMPLSP1:def 7
.= (c * x) + ((c multcomplex ) * y) by COMPLSP1:def 10
.= (c * x) + (c * y) by COMPLSP1:def 10 ;
hence c * (x + y) = (c * x) + (c * y) ; :: thesis: verum