take Dir100 ; :: thesis:
reconsider p = |[1,0,0]| as non zero Element of (TOP-REAL 3) ;

let u be non zero Element of (TOP-REAL 3); :: thesis:
assume Dir100 = Dir u ; :: thesis:
then are_Prop u,p by ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A1: u = a * p by ANPROJ_1:1;
A2: |[1,0,0]| = |[(p . 1),(p . 2),(p . 3)]| by EUCLID_8:1, EUCLID_8:def 1;
thus u . 3 = a * (p . 3) by A1, RVSUM_1:44
.= a * 0 by A2, FINSEQ_1:78
.= 0 ; :: thesis:

end;