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:110;
mlt z,(x + y) = mlt (x2 + y2),z2 by FVSUM_1:77
.= (mlt x2,z2) + (mlt y,z) by A1, Th56
.= (mlt z,x) + (mlt y2,z2) by FVSUM_1:77 ;
hence mlt z,(x + y) = (mlt z,x) + (mlt z,y) by FVSUM_1:77; :: thesis: verum