let x1, x2, y1, y2 be FinSequence of REAL ; :: 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 RVSUM_1:75;
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, Th14;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + (Sum (mlt (y1,y2))) by RVSUM_1:def 16;
then |((x1 ^ y1),(x2 ^ y2))| = (Sum (mlt (x1,x2))) + |(y1,y2)| by RVSUM_1:def 16;
hence |((x1 ^ y1),(x2 ^ y2))| = |(x1,x2)| + |(y1,y2)| by RVSUM_1:def 16; :: thesis: verum