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

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