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)| )
A1: ( x is FinSequence of REAL & y is FinSequence of REAL & z is FinSequence of REAL ) by Lm2;
assume A2: ( 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 A1, FINSEQ_2:92;
|((x + y),z)| = Sum ((mlt (x,z)) + (mlt (y,z))) by A2, Th118
.= (Sum (mlt (x2,z2))) + (Sum (mlt (y2,z2))) by Th89
.= |(x,z)| + |(y,z)| ;
hence |((x + y),z)| = |(x,z)| + |(y,z)| ; :: thesis: verum