let u, v be non zero Element of (TOP-REAL 3); :: thesis: ( Dir u = P & u . 3 = 1 & Dir v = P & v . 3 = 1 implies u = v )
assume that
A4: ( P = Dir u & u . 3 = 1 ) and
A5: ( P = Dir v & v . 3 = 1 ) ; :: thesis: u = v
are_Prop u,v by A4, A5, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A6: u = a * v by ANPROJ_1:1;
A7: 1 = a * (v . 3) by A4, A6, RVSUM_1:44
.= a by A5 ;
a * v = |[(a * (v `1)),(a * (v `2)),(a * (v `3))]| by EUCLID_5:7
.= v by A7, EUCLID_5:3 ;
hence u = v by A6; :: thesis: verum