let x, y, z be FinSequence of COMPLEX ; :: thesis: ( len x = len y & len y = len z implies mlt (x - y),z = (mlt x,z) - (mlt y,z) )
assume that
A1: len x = len y and
A2: len y = len z ; :: thesis: mlt (x - y),z = (mlt x,z) - (mlt y,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,z2) - (mlt y2,z2))) by FINSEQ_1:def 18
.= dom ((mlt x2,z2) - (mlt y2,z2)) by FINSEQ_1:def 3 ;
A4: 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 ;
A5: dom (mlt y,z) = Seg (len (mlt 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 ;
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 A6: 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 A7: (x - y) . i = (x . i) - (y . i) by A3, A4, A6, COMPLSP2:2;
thus (mlt (x - y),z) . i = ((x - y) . i) * (z . i) by A6, Th19
.= ((x . i) * (z . i)) - ((y . i) * (z . i)) by A7
.= ((mlt x,z) . i) - ((y . i) * (z . i)) by A3, A4, A6, Th19
.= ((mlt x,z) . i) - ((mlt y,z) . i) by A3, A5, A6, Th19
.= ((mlt x,z) - (mlt y,z)) . i by A3, A6, COMPLSP2:2 ; :: thesis: verum

end;

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