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;

( 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 ) )

hence
H1 = H2
by FUNCT_1:def 11; :: thesis: verumfH1 . 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

end;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;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