consider u being non zero Element of (TOP-REAL 3) such that
A1: P = Dir u and
A2: u . 1 <> 0 by Def1;
reconsider v = |[1,((u `2) / (u . 1)),((u `3) / (u . 1))]| as non zero Element of (TOP-REAL 3) ;
take v ; :: thesis: ( Dir v = P & v . 1 = 1 )
(u . 1) * v = |[((u . 1) * 1),((u . 1) * ((u `2) / (u . 1))),((u . 1) * ((u `3) / (u . 1)))]| by EUCLID_5:8
.= |[(u . 1),(u `2),((u . 1) * ((u `3) / (u . 1)))]| by XCMPLX_1:87, A2
.= |[(u `1),(u `2),(u `3)]| by A2, XCMPLX_1:87
.= u by EUCLID_5:3 ;
then are_Prop u,v by A2, ANPROJ_1:1;
hence ( Dir v = P & v . 1 = 1 ) by A1, ANPROJ_1:22; :: thesis: verum