let x, y, z be FinSequence of REAL ; :: thesis: ( len x = len y & len y = len z implies |((x + y),z)| = |(x,z)| + |(y,z)| )
assume A1: ( len x = len y & len y = len z ) ; :: thesis: |((x + y),z)| = |(x,z)| + |(y,z)|
then reconsider x2 = x, y2 = y, z2 = z as Element of (len x) -tuples_on REAL by FINSEQ_2:110;
|((x + y),z)| = Sum ((mlt x,z) + (mlt y,z)) by A1, Th9
.= (Sum (mlt x2,z2)) + (Sum (mlt y2,z2)) by RVSUM_1:119
.= |(x,z)| + |(y,z)| ;
hence |((x + y),z)| = |(x,z)| + |(y,z)| ; :: thesis: verum