theorem Th17: :: ANPROJ11:17

for P being non zero_proj3 Point of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st P = Dir u holds
normalize_proj3 P = |[((u . 1) / (u . 3)),((u . 2) / (u . 3)),1]|