let u, v be non zero Element of (TOP-REAL 3); :: thesis: ( Dir u = Dir v & u . 3 <> 0 & u . 3 = v . 3 implies u = v )
assume that
A1: Dir u = Dir v and
A2: u . 3 <> 0 and
A3: u . 3 = v . 3 ; :: thesis: u = v
are_Prop u,v by A1, ANPROJ_1:22;
then consider a being Real such that
a <> 0 and
A4: u = a * v by ANPROJ_1:1;
u . 3 = a * (u . 3) by A3, A4, RVSUM_1:44;
then a = 1 by A2, XCMPLX_1:7;
hence u = v by A4, RVSUM_1:52; :: thesis: verum