theorem :: ANPROJ11:32

for P being non zero_proj1 non zero_proj2 Point of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
( normalize_proj1 P = ((u . 2) / (u . 1)) * (normalize_proj2 P) & normalize_proj2 P = ((u . 1) / (u . 2)) * (normalize_proj1 P) )