let K be Field; :: thesis: for x, y, z being FinSequence of K st len x = len y & len y = len z holds
mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))
let x, y, z be FinSequence of K; :: thesis: ( len x = len y & len y = len z implies mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) )
assume A1: ( len x = len y & len y = len z ) ; :: thesis: mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y))
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on the carrier of K by FINSEQ_2:92;
mlt (z,(x + y)) = mlt ((x2 + y2),z2) by FVSUM_1:63
.= (mlt (x2,z2)) + (mlt (y,z)) by A1, Th56
.= (mlt (z,x)) + (mlt (y2,z2)) by FVSUM_1:63 ;
hence mlt (z,(x + y)) = (mlt (z,x)) + (mlt (z,y)) by FVSUM_1:63; :: thesis: verum