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: abs (||.v.|| ") = abs (1 * (||.v.|| "))
.= abs (1 / ||.v.||) by XCMPLX_0:def 9
.= 1 / (abs ||.v.||) by ABSVALUE:7
.= 1 * ((abs ||.v.||) ") by XCMPLX_0:def 9
.= ||.v.|| " by A3, ABSVALUE:def 1 ;
thus ||.w.|| = (abs (||.v.|| ")) * ||.v.|| by NORMSP_1:def 1
.= 1 by A2, A4, XCMPLX_0:def 7 ; :: thesis: verum