let P, Q, R, S, T, U be Element of BK_model ; :: thesis: ( ex h1, h2 being Element of SubGroupK-isometry ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & (homography N1) . P = R & (homography N1) . Q = S & (homography N2) . R = T & (homography N2) . S = U ) implies ex h3 being Element of SubGroupK-isometry ex N3 being invertible Matrix of 3,F_Real st
( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U ) )
assume ex h1, h2 being Element of SubGroupK-isometry ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & (homography N1) . P = R & (homography N1) . Q = S & (homography N2) . R = T & (homography N2) . S = U ) ; :: thesis: ex h3 being Element of SubGroupK-isometry ex N3 being invertible Matrix of 3,F_Real st
( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U )
then consider h1, h2 being Element of SubGroupK-isometry, N1, N2 being invertible Matrix of 3,F_Real such that
A1: ( h1 = homography N1 & h2 = homography N2 & (homography N1) . P = R & (homography N1) . Q = S & (homography N2) . R = T & (homography N2) . S = U ) ;
reconsider N3 = N2 * N1 as invertible Matrix of 3,F_Real ;
h2 * h1 = homography (N2 * N1) by A1, Th35;
then reconsider h3 = homography N3 as Element of SubGroupK-isometry ;
take h3 ; :: thesis: ex N3 being invertible Matrix of 3,F_Real st
( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U )
( (homography N3) . P = T & (homography N3) . Q = U ) by A1, ANPROJ_9:13;
hence ex N3 being invertible Matrix of 3,F_Real st
( h3 = homography N3 & (homography N3) . P = T & (homography N3) . Q = U ) ; :: thesis: verum