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 that
A1: len x = len y and
A2: len y = len z ; :: thesis: mlt x,(y + z) = (mlt x,y) + (mlt x,z)
reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A1, A2, FINSEQ_2:110;
A3: 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 ;
A4: 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 ;
A5: 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 A6: i in dom (mlt x,(y + z)) ; :: thesis: (mlt x,(y + z)) . i = ((mlt x,y) + (mlt x,z)) . i
set a = y . i;
set b = z . i;
set d = (y + z) . i;
set e = x . i;
len (y2 + z2) = len x by FINSEQ_1:def 18;
then 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 ;
then A7: (y + z) . i = (y . i) + (z . i) by A3, A4, A6, COMPLSP2:1;
thus (mlt x,(y + z)) . i = (x . i) * ((y + z) . i) by A6, Th19
.= ((x . i) * (y . i)) + ((x . i) * (z . i)) by A7
.= ((mlt x,y) . i) + ((x . i) * (z . i)) by A3, A4, A6, Th19
.= ((mlt x,y) . i) + ((mlt x,z) . i) by A3, A5, A6, Th19
.= ((mlt x,y) + (mlt x,z)) . i by A3, A6, COMPLSP2:1 ; :: thesis: verum

end;

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