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 19;
A2: ||.v.|| <> 0 by A1, CLVECT_1:def 11;
then A3: 0 < ||.v.|| by CLVECT_1:106;
reconsider a = ||.v.|| + (0 * <i> ) as Element of COMPLEX by XCMPLX_0:def 2;
A4: |.(a " ).| = |.(1r * (a " )).| by COMPLEX1:def 7
.= |.(1r / a).| by XCMPLX_0:def 9
.= 1 / |.a.| by COMPLEX1:134, COMPLEX1:153
.= 1 * (|.a.| " ) by XCMPLX_0:def 9
.= ||.v.|| " by A3, ABSVALUE:def 1 ;
take w = (a " ) * v; :: thesis: ||.w.|| = 1
thus ||.w.|| = |.(a " ).| * ||.v.|| by CLVECT_1:def 11
.= 1 by A2, A4, XCMPLX_0:def 7 ; :: thesis: verum