theorem Th11: :: ANPROJ11:11

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