for N1, N2 being invertible Matrix of 3,F_Real
for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds (line_homography N1) . ((line_homography N2) . l) = (line_homography (N1 * N2)) . l