let K be Field; :: thesis: for x, y1, y2 being FinSequence of K
for a being Element of K st len x = len y1 & len x = len y2 holds
|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|
let x, y1, y2 be FinSequence of K; :: thesis: for a being Element of K st len x = len y1 & len x = len y2 holds
|(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|
let a be Element of K; :: thesis: ( len x = len y1 & len x = len y2 implies |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| )
reconsider x0 = x as Element of (len x) -tuples_on the carrier of K by Th1;
assume A1: ( len x = len y1 & len x = len y2 ) ; :: thesis: |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)|
then reconsider y10 = y1, y20 = y2 as Element of (len x) -tuples_on the carrier of K by Th1;
Sum (mlt (x,(y1 + y2))) = Sum ((mlt (x0,y10)) + (mlt (x0,y20))) by A1, MATRIX_4:57;
then Sum (mlt (x,(y1 + y2))) = (Sum (mlt (x0,y10))) + (Sum (mlt (x0,y20))) by FVSUM_1:76;
then Sum (mlt (x,(y1 + y2))) = (Sum (mlt (x,y1))) + |(x,y2)| by FVSUM_1:def 9;
then Sum (mlt (x,(y1 + y2))) = |(x,y1)| + |(x,y2)| by FVSUM_1:def 9;
hence |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| by FVSUM_1:def 9; :: thesis: verum