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