let h, g be Element of GroupLineHomography3; :: thesis: for N, Ng being invertible Matrix of 3,F_Real st h = line_homography N & g = line_homography Ng & Ng = N ~ holds
g = h "
let N, Ng be invertible Matrix of 3,F_Real; :: thesis: ( h = line_homography N & g = line_homography Ng & Ng = N ~ implies g = h " )
assume ( h = line_homography N & g = line_homography Ng & Ng = N ~ ) ; :: thesis: g = h "
then ( h * g = 1_ GroupLineHomography3 & g * h = 1_ GroupLineHomography3 ) by Lm2, Th18;
hence g = h " by GROUP_1:def 5; :: thesis: verum