let h be Element of EnsK-isometry ; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N holds
(homography N) .: absolute = absolute
let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N implies (homography N) .: absolute = absolute )
assume A1: h = homography N ; :: thesis: (homography N) .: absolute = absolute
h in { h where h is Element of EnsHomography3 : h is_K-isometry } ;
then consider g being Element of EnsHomography3 such that
A2: h = g and
A3: g is_K-isometry ;
thus (homography N) .: absolute = absolute by A1, A2, A3; :: thesis: verum