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)| )
A1: Sum ((mlt (x1,x2)) ^ (mlt (y1,y2))) = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by RLVECT_1:41;
assume ( len x1 = len x2 & len y1 = len y2 ) ; :: thesis: |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)|
then Sum (mlt ((x1 ^ y1),(x2 ^ y2))) = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by A1, Th7;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by FVSUM_1:def 9;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + |(y1,y2)| by FVSUM_1:def 9;
hence |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| by FVSUM_1:def 9; :: thesis: verum