theorem Th17: :: NDIFF13:16

for X, Y being RealNormSpace
for x being Point of X
for y being Point of Y
for z being Point of [:X,Y:] st z = [x,y] holds
||.z.|| <= ||.x.|| + ||.y.||