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)) )
A1: ( x is FinSequence of COMPLEX & y is FinSequence of COMPLEX & z is FinSequence of COMPLEX ) by Lm2;
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 A1, FINSEQ_2:92;
A2: dom (mlt ((x + y),z)) = Seg (len (mlt ((x2 + y2),z2))) by FINSEQ_1:def 3
.= Seg (len x) by CARD_1:def 7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def 7
.= dom ((mlt (x2,z2)) + (mlt (y2,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 CARD_1:def 7
.= Seg (len ((mlt (x2,z2)) + (mlt (y2,z2)))) by CARD_1:def 7
.= 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 CARD_1:def 7;
then dom (x2 + y2) = Seg (len x) by FINSEQ_1:def 3
.= Seg (len (mlt (x2,z2))) by CARD_1:def 7
.= dom (mlt (x,z)) by FINSEQ_1:def 3 ;
then A5: (x + y) . i = (x . i) + (y . i) by A2, A3, 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 A2, A4, VALUED_1:def 1 ; :: thesis: verum

end;

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