let N1, N2 be invertible Matrix of 3,F_Real; :: thesis: for h1, h2 being Element of SubGroupK-isometry st h1 = homography N1 & h2 = homography N2 holds
( h1 * h2 is Element of SubGroupK-isometry & h1 * h2 = homography (N1 * N2) )
let h1, h2 be Element of SubGroupK-isometry; :: thesis: ( h1 = homography N1 & h2 = homography N2 implies ( h1 * h2 is Element of SubGroupK-isometry & h1 * h2 = homography (N1 * N2) ) )
assume that
A1: h1 = homography N1 and
A2: h2 = homography N2 ; :: thesis: ( h1 * h2 is Element of SubGroupK-isometry & h1 * h2 = homography (N1 * N2) )
thus h1 * h2 is Element of SubGroupK-isometry ; :: thesis: h1 * h2 = homography (N1 * N2)
h1 in EnsHomography3 by A1, ANPROJ_9:def 1;
then reconsider hh1 = h1 as Element of EnsHomography3 ;
h2 in EnsHomography3 by A2, ANPROJ_9:def 1;
then reconsider hh2 = h2 as Element of EnsHomography3 ;
set G = GroupHomography3 ;
reconsider h1g = hh1, h2g = hh2 as Element of GroupHomography3 by ANPROJ_9:def 4;
h1g * h2g = hh1 (*) hh2 by ANPROJ_9:def 3, ANPROJ_9:def 4
.= homography (N1 * N2) by A1, A2, ANPROJ_9:18 ;
hence h1 * h2 = homography (N1 * N2) by GROUP_2:43; :: thesis: verum