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