for N1 being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for a being non zero Element of F_Real holds (homography (a * N1)) . P = (homography N1) . P