let K be Field; :: thesis: for x1, x2, y1, y2 being FinSequence of K st len x1 = len x2 & len y1 = len y2 holds
|((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|
let x1, x2, y1, y2 be FinSequence of K; :: thesis: ( len x1 = len x2 & len y1 = len y2 implies |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| )
assume A1: ( len x1 = len x2 & len y1 = len y2 ) ; :: thesis: |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|
Sum ((mlt x1,x2) ^ (mlt y1,y2)) = (Sum (mlt x1,x2)) + (Sum (mlt y1,y2)) by RLVECT_1:58;
then Sum (mlt (x1 ^ y1),(x2 ^ y2)) = (Sum (mlt x1,x2)) + (Sum (mlt y1,y2)) by BB240, A1;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt x1,x2)) + (Sum (mlt y1,y2)) by FVSUM_1:def 10;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt x1,x2)) + |(y1,y2)| by FVSUM_1:def 10;
hence |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| by FVSUM_1:def 10; :: thesis: verum