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

( 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