let P be Element of absolute ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st
( ((u . 1) ^2) + ((u . 2) ^2) = 1 & u . 3 = 1 & P = Dir u )
consider u being Element of (TOP-REAL 3) such that
A1: not u is zero and
A2: Dir u = P by ANPROJ_1:26;
reconsider v1 = (u . 1) / (u . 3), v2 = (u . 2) / (u . 3) as Real ;
reconsider v = |[v1,v2,1]| as Element of (TOP-REAL 3) ;
A3: v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
A4: not v is zero by EUCLID_5:4, FINSEQ_1:78;
(u . 3) * v = |[((u . 3) * v1),((u . 3) * v2),((u . 3) * 1)]| by EUCLID_5:8
.= |[(u . 1),((u . 3) * v2),(u . 3)]| by A1, A2, Th67, XCMPLX_1:87
.= |[(u . 1),(u . 2),(u . 3)]| by A1, A2, Th67, XCMPLX_1:87
.= |[(u `1),(u . 2),(u . 3)]| by EUCLID_5:def 1
.= |[(u `1),(u `2),(u . 3)]| by EUCLID_5:def 2
.= |[(u `1),(u `2),(u `3)]| by EUCLID_5:def 3
.= u by EUCLID_5:3 ;
then are_Prop u,v by A1, A2, Th67, ANPROJ_1:1;
then A5: Dir v = Dir u by A1, A4, ANPROJ_1:22;
|[(v . 1),(v . 2)]| in circle (0,0,1) by A2, A3, A4, A5, Th68;
then ((v . 1) ^2) + ((v . 2) ^2) = 1 ^2 by Th12
.= 1 ;
hence ex u being non zero Element of (TOP-REAL 3) st
( ((u . 1) ^2) + ((u . 2) ^2) = 1 & u . 3 = 1 & P = Dir u ) by A2, A3, A4, A5; :: thesis: verum