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

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