let K be Field; 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; ( 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 )
; 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; verum