let N be invertible Matrix of 3,F_Real; :: thesis: dom (homography N) = ProjectivePoints (TOP-REAL 3)
dom (homography N) = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence dom (homography N) = ProjectivePoints (TOP-REAL 3) by ANPROJ_1:23; :: thesis: verum