let P, Q, R, S, T, U be Element of BK_model ; ( 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 )
; 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
; 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 )
; verum