theorem LM0: :: NDIFF_9:6

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