let X be non trivial ComplexNormSpace; :: 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;
reconsider a = ||.v.|| + (0 * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
take w = (a ") * v; :: thesis: ||.w.|| = 1
A2: ||.v.|| <> 0 by A1, NORMSP_0:def 5;
then A3: 0 < ||.v.|| by CLVECT_1:105;
A4: |.(a ").| = |.(1r * (a ")).| by COMPLEX1:def 4
.= |.(1r / a).| by XCMPLX_0:def 9
.= 1 / |.a.| by COMPLEX1:48, COMPLEX1:67
.= 1 * (|.a.| ") by XCMPLX_0:def 9
.= ||.v.|| " by A3, ABSVALUE:def 1 ;
thus ||.w.|| = |.(a ").| * ||.v.|| by CLVECT_1:def 13
.= 1 by A2, A4, XCMPLX_0:def 7 ; :: thesis: verum