let X, Y be RealNormSpace; :: thesis: for y being Point of Y
for z being Point of [:X,Y:] st z = [(0. X),y] holds
||.z.|| = ||.y.||
let y be Point of Y; :: thesis: for z being Point of [:X,Y:] st z = [(0. X),y] holds
||.z.|| = ||.y.||
let z be Point of [:X,Y:]; :: thesis: ( z = [(0. X),y] implies ||.z.|| = ||.y.|| )
assume z = [(0. X),y] ; :: thesis: ||.z.|| = ||.y.||
then ||.z.|| = sqrt ((||.(0. X).|| ^2) + (||.y.|| ^2)) by LMNR0
.= sqrt (||.y.|| ^2) ;
hence ||.y.|| = ||.z.|| by SQUARE_1:22; :: thesis: verum