for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds (homography (1. (F_Real,3))) . P = P