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

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