let x, y, z be complex-valued FinSequence; :: thesis: ( len x = len y & len y = len z implies mlt (x + y),z = (mlt x,z) + (mlt y,z) )
A0: ( x is FinSequence of COMPLEX & y is FinSequence of COMPLEX & z is FinSequence of COMPLEX ) by Lm4;
assume ( len x = len y & len y = len z ) ; :: thesis: mlt (x + y),z = (mlt x,z) + (mlt y,z)
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on COMPLEX by A0, 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,z2) + (mlt y2,z2))) by FINSEQ_1:def 18
.= dom ((mlt x2,z2) + (mlt y2,z2)) by FINSEQ_1:def 3 ;
A2: 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,z2) + (mlt y2,z2))) by FINSEQ_1:def 18
.= dom ((mlt x2,z2) + (mlt y2,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,z) + (mlt y,z)) . i

proof

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

end;

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