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