for x, y, z being real-valued FinSequence st len x = len y & len y = len z holds
|((x + y),z)| = |(x,z)| + |(y,z)|