theorem :: BKMODEL1:80

for N being invertible Matrix of 3,F_Real holds dom (homography N) = ProjectivePoints (TOP-REAL 3)