let h1, h2 be Function of the Lines of (IncProjSp_of real_projective_plane), the Lines of (IncProjSp_of real_projective_plane); :: thesis: ( ( for x being LINE of (IncProjSp_of real_projective_plane) holds h1 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ) & ( for x being LINE of (IncProjSp_of real_projective_plane) holds h2 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ) implies h1 = h2 )

assume that

A14: for x being LINE of (IncProjSp_of real_projective_plane) holds h1 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } and

A15: for x being LINE of (IncProjSp_of real_projective_plane) holds h2 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ; :: thesis: h1 = h2

assume that

A14: for x being LINE of (IncProjSp_of real_projective_plane) holds h1 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } and

A15: for x being LINE of (IncProjSp_of real_projective_plane) holds h2 . x = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on x } ; :: thesis: h1 = h2

now :: thesis: ( dom h1 = dom h2 & ( for x9 being object st x9 in dom h1 holds

h1 . x9 = h2 . x9 ) )

hence
h1 = h2
by FUNCT_1:def 11; :: thesis: verumh1 . x9 = h2 . x9 ) )

dom h1 = the Lines of (IncProjSp_of real_projective_plane)
by FUNCT_2:def 1;

hence dom h1 = dom h2 by FUNCT_2:def 1; :: thesis: for x9 being object st x9 in dom h1 holds

h1 . x9 = h2 . x9

end;hence dom h1 = dom h2 by FUNCT_2:def 1; :: thesis: for x9 being object st x9 in dom h1 holds

h1 . x9 = h2 . x9

hereby :: thesis: verum

let x9 be object ; :: thesis: ( x9 in dom h1 implies h1 . x9 = h2 . x9 )

assume x9 in dom h1 ; :: thesis: h1 . x9 = h2 . x9

then reconsider y = x9 as LINE of (IncProjSp_of real_projective_plane) ;

h1 . y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on y } by A14

.= h2 . y by A15 ;

hence h1 . x9 = h2 . x9 ; :: thesis: verum

end;assume x9 in dom h1 ; :: thesis: h1 . x9 = h2 . x9

then reconsider y = x9 as LINE of (IncProjSp_of real_projective_plane) ;

h1 . y = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on y } by A14

.= h2 . y by A15 ;

hence h1 . x9 = h2 . x9 ; :: thesis: verum