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
A3: ( Dir u = P & u . 3 = 1 ) and
A4: ( Dir v = P & v . 3 = 1 ) ; :: thesis: u = v
are_Prop u,v by A3, A4, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A5: u = a * v by ANPROJ_1:1;
1 = a * (v . 3) by A5, A3, RVSUM_1:44
.= a by A4 ;
hence u = v by A5, RVSUM_1:52; :: thesis: verum