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