let x1, x2, y1, y2 be FinSequence of REAL ; ( 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 )
; |((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; verum