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

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