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
now :: thesis: ( dom h1 = dom h2 & ( for x9 being object st x9 in dom h1 holds
h1 . 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
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;
end;
hence h1 = h2 by FUNCT_1:def 11; :: thesis: verum