theorem :: ANPROJ11:22

for P being non zero_proj1 Element of (ProjectiveSpace (TOP-REAL 3))
for u being non zero Element of (TOP-REAL 3) st u = normalize_proj1 P holds
|{(dir1a P),(dir1b P),(normalize_proj1 P)}| = (1 + ((u . 2) * (u . 2))) + ((u . 3) * (u . 3))