theorem :: ANPROJ11:26

for P being non zero_proj2 Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st u = normalize_proj2 P holds
|{(dir2a P),(dir2b P),(normalize_proj2 P)}| = - ((((u . 1) * (u . 1)) + 1) + ((u . 3) * (u . 3)))