let x, y, z be real-valued FinSequence; :: thesis: ( len x = len y & len y = len z implies |((x + y),z)| = |(x,z)| + |(y,z)| )
A0: ( x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL ) by Lm4;
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 A0, 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 Th119
.= |(x,z)| + |(y,z)| ;
hence |((x + y),z)| = |(x,z)| + |(y,z)| ; :: thesis: verum