let H1, H2 be Element of EnsLineHomography3 ; :: thesis: ( ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & H1 = line_homography (N1 * N2) ) & ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & H2 = line_homography (N1 * N2) ) implies H1 = H2 )
assume that
A3: ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & H1 = line_homography (N1 * N2) ) and
A4: ex N1, N2 being invertible Matrix of 3,F_Real st
( h1 = line_homography N1 & h2 = line_homography N2 & H2 = line_homography (N1 * N2) ) ; :: thesis: H1 = H2
consider NA1, NA2 being invertible Matrix of 3,F_Real such that
A5: h1 = line_homography NA1 and
A6: h2 = line_homography NA2 and
A7: H1 = line_homography (NA1 * NA2) by A3;
consider NB1, NB2 being invertible Matrix of 3,F_Real such that
A8: h1 = line_homography NB1 and
A9: h2 = line_homography NB2 and
A10: H2 = line_homography (NB1 * NB2) by A4;
reconsider fH1 = H1, fH2 = H2 as Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane) 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 Lines of (IncProjSp_of real_projective_plane) 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 the Lines of (IncProjSp_of real_projective_plane) ;
fH1 . x = (line_homography NB1) . ((line_homography NB2) . P) by A5, A6, A7, A8, A9, Th13
.= fH2 . x by A10, Th13 ;
hence fH1 . x = fH2 . x ; :: thesis: verum
end;
end;
hence H1 = H2 by FUNCT_1:def 11; :: thesis: verum