let P be non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: Dir (dir3a P) <> Dir (dir3b P)
assume Dir (dir3a P) = Dir (dir3b P) ; :: thesis: contradiction
then are_Prop dir3a P, dir3b P by ANPROJ_1:22;
then consider a being Real such that
A1: a <> 0 and
A2: dir3a P = a * (dir3b P) by ANPROJ_1:1;
0 = (dir3a P) `2
.= a * ((dir3b P) `2) by A2, RVSUM_1:44
.= a * 1 ;
hence contradiction by A1; :: thesis: verum