for N1, N2 being invertible Matrix of 3,F_Real
for h1, h2 being Element of EnsLineHomography3 st h1 = line_homography N1 & h2 = line_homography N2 holds
line_homography (N1 * N2) = h1 (*) h2