h1 in { (homography N) where N is invertible Matrix of 3,F_Real : verum }
;

then consider N1 being invertible Matrix of 3,F_Real such that

A1: h1 = homography N1 ;

h2 in { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;

then consider N2 being invertible Matrix of 3,F_Real such that

A2: h2 = homography N2 ;

homography (N1 * N2) in EnsHomography3 ;

hence ex b_{1} being Element of EnsHomography3 ex N1, N2 being invertible Matrix of 3,F_Real st

( h1 = homography N1 & h2 = homography N2 & b_{1} = homography (N1 * N2) )
by A1, A2; :: thesis: verum

then consider N1 being invertible Matrix of 3,F_Real such that

A1: h1 = homography N1 ;

h2 in { (homography N) where N is invertible Matrix of 3,F_Real : verum } ;

then consider N2 being invertible Matrix of 3,F_Real such that

A2: h2 = homography N2 ;

homography (N1 * N2) in EnsHomography3 ;

hence ex b

( h1 = homography N1 & h2 = homography N2 & b