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