theorem :: ANPROJ_9:16

for N being invertible Matrix of 3,F_Real
for P1, P2 being Point of (ProjectiveSpace (TOP-REAL 3)) st (homography N) . P1 = (homography N) . P2 holds
P1 = P2