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:95;
then Sum (mlt x,(y1 + y2)) = (Sum (mlt x,y1)) + |(x,y2)| by FVSUM_1:def 10;
then Sum (mlt x,(y1 + y2)) = |(x,y1)| + |(x,y2)| by FVSUM_1:def 10;
hence |(x,(y1 + y2))| = |(x,y1)| + |(x,y2)| by FVSUM_1:def 10; :: thesis: verum