let H1, H2 be Element of EnsHomography3 ; :: thesis: ( ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & H1 = homography (N1 * N2) ) & ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & H2 = homography (N1 * N2) ) implies H1 = H2 )
assume that
A3: ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & H1 = homography (N1 * N2) ) and
A4: ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = homography N1 & h2 = homography N2 & H2 = homography (N1 * N2) ) ; :: thesis: H1 = H2
consider NA1, NA2 being invertible Matrix of 3,F_Real such that
A5: h1 = homography NA1 and
A6: h2 = homography NA2 and
A7: H1 = homography (NA1 * NA2) by A3;
consider NB1, NB2 being invertible Matrix of 3,F_Real such that
A8: h1 = homography NB1 and
A9: h2 = homography NB2 and
A10: H2 = homography (NB1 * NB2) by A4;
reconsider fH1 = H1, fH2 = H2 as Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) by A7, A10;

now :: thesis: ( dom fH1 = dom fH2 & ( for x being object st x in dom fH1 holds
fH1 . x = fH2 . x ) )

dom fH1 = the carrier of (ProjectiveSpace (TOP-REAL 3)) by FUNCT_2:def 1;
hence dom fH1 = dom fH2 by FUNCT_2:def 1; :: thesis: for x being object st x in dom fH1 holds
fH1 . x = fH2 . x
thus for x being object st x in dom fH1 holds
fH1 . x = fH2 . x :: thesis: verum

proof

let x be object ; :: thesis: ( x in dom fH1 implies fH1 . x = fH2 . x )
assume x in dom fH1 ; :: thesis: fH1 . x = fH2 . x
then reconsider P = x as Element of (ProjectiveSpace (TOP-REAL 3)) ;
fH1 . x = (homography NB1) . ((homography NB2) . P) by A5, A6, A7, A8, A9, Th14
.= fH2 . x by A10, Th14 ;
hence fH1 . x = fH2 . x ; :: thesis: verum

end;

end;

hence H1 = H2 by FUNCT_1:def 11; :: thesis: verum