theorem :: ANPROJ11:30

for P being non zero_proj3 Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st u = normalize_proj3 P holds
|{(dir3a P),(dir3b P),(normalize_proj3 P)}| = (((u . 1) * (u . 1)) + ((u . 2) * (u . 2))) + 1