let P be Element of absolute ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st
( u . 3 = 1 & P = Dir u )
consider u being Element of (TOP-REAL 3) such that
A1: not u is zero and
A2: P = Dir u by ANPROJ_1:26;
u . 3 <> 0 by A1, A2, BKMODEL1:83;
then A3: u `3 <> 0 by EUCLID_5:def 3;
reconsider v = |[((u `1) / (u `3)),((u `2) / (u `3)),1]| as non zero Element of (TOP-REAL 3) ;
take v ; :: thesis: ( v . 3 = 1 & P = Dir v )
thus v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: P = Dir v
(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) * 1)]| by A3, XCMPLX_1:87
.= |[(u `1),(u `2),((u `3) * 1)]| by A3, XCMPLX_1:87
.= u by EUCLID_5:3 ;
then are_Prop u,v by A3, ANPROJ_1:1;
hence P = Dir v by A1, A2, ANPROJ_1:22; :: thesis: verum