let x, y, z be FinSequence of COMPLEX ; :: thesis: ( len x = len y & len y = len z implies mlt x,(y + z) = (mlt x,y) + (mlt x,z) )
assume ( len x = len y & len y = len z ) ; :: thesis: mlt x,(y + z) = (mlt x,y) + (mlt x,z)
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by FINSEQ_2:110;
A1: dom (mlt x,(y + z)) = Seg (len (mlt x2,(y2 + z2))) by FINSEQ_1:def 3
.= Seg (len x) by FINSEQ_1:def 18
.= Seg (len ((mlt x2,y2) + (mlt x2,z2))) by FINSEQ_1:def 18
.= dom ((mlt x2,y2) + (mlt x2,z2)) by FINSEQ_1:def 3 ;
A2: dom (mlt x,y) = Seg (len (mlt x2,y2)) by FINSEQ_1:def 3
.= Seg (len x) by FINSEQ_1:def 18
.= Seg (len ((mlt x2,y2) + (mlt x2,z2))) by FINSEQ_1:def 18
.= dom ((mlt x2,y2) + (mlt x2,z2)) by FINSEQ_1:def 3 ;
A3: dom (mlt x,z) = Seg (len (mlt x2,z2)) by FINSEQ_1:def 3
.= Seg (len x) by FINSEQ_1:def 18
.= Seg (len ((mlt x2,y2) + (mlt x2,z2))) by FINSEQ_1:def 18
.= dom ((mlt x2,y2) + (mlt x2,z2)) by FINSEQ_1:def 3 ;
for i being Nat st i in dom (mlt x,(y + z)) holds
(mlt x,(y + z)) . i = ((mlt x,y) + (mlt x,z)) . i

proof

let i be Nat; :: thesis: ( i in dom (mlt x,(y + z)) implies (mlt x,(y + z)) . i = ((mlt x,y) + (mlt x,z)) . i )
assume A4: i in dom (mlt x,(y + z)) ; :: thesis: (mlt x,(y + z)) . i = ((mlt x,y) + (mlt x,z)) . i
len (y2 + z2) = len x by FINSEQ_1:def 18;
then A5: dom (y2 + z2) = Seg (len x) by FINSEQ_1:def 3
.= Seg (len (mlt x2,y2)) by FINSEQ_1:def 18
.= dom (mlt x,y) by FINSEQ_1:def 3 ;
set a = y . i;
set b = z . i;
set d = (y + z) . i;
set e = x . i;
A6: (y + z) . i = (y . i) + (z . i) by A1, A2, A4, A5, COMPLSP2:1;
thus (mlt x,(y + z)) . i = (x . i) * ((y + z) . i) by A4, Th19
.= ((x . i) * (y . i)) + ((x . i) * (z . i)) by A6
.= ((mlt x,y) . i) + ((x . i) * (z . i)) by A1, A2, A4, Th19
.= ((mlt x,y) . i) + ((mlt x,z) . i) by A1, A3, A4, Th19
.= ((mlt x,y) + (mlt x,z)) . i by A1, A4, COMPLSP2:1 ; :: thesis: verum

end;

hence mlt x,(y + z) = (mlt x,y) + (mlt x,z) by A1, FINSEQ_1:17; :: thesis: verum