theorem :: NDIFF_8:3

for X, Y being RealNormSpace
for y being Point of Y
for z being Point of [:X,Y:] st z = [(0. X),y] holds
||.z.|| = ||.y.||