let X be non trivial RealNormSpace; :: thesis: ex w being VECTOR of X st ||.w.|| = 1
consider v being VECTOR of X such that
A1: v <> 0. X by STRUCT_0:def 18;
set a = ||.v.||;
reconsider w = (||.v.|| ") * v as VECTOR of X ;
take w ; :: thesis: ||.w.|| = 1
A2: ||.v.|| <> 0 by A1, NORMSP_0:def 5;
then A3: 0 < ||.v.|| by NORMSP_1:4;
A4: |.(||.v.|| ").| = |.(1 * (||.v.|| ")).|
.= |.(1 / ||.v.||).| by XCMPLX_0:def 9
.= 1 / |.||.v.||.| by ABSVALUE:7
.= 1 * (|.||.v.||.| ") by XCMPLX_0:def 9
.= ||.v.|| " by A3, ABSVALUE:def 1 ;
thus ||.w.|| = |.(||.v.|| ").| * ||.v.|| by NORMSP_1:def 1
.= 1 by A2, A4, XCMPLX_0:def 7 ; :: thesis: verum