theorem LMNR0: :: NDIFF_8:1

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.|| = sqrt ((||.x.|| ^2) + (||.y.|| ^2))