let N be invertible Matrix of 3,F_Real; :: thesis: for P1, P2 being Point of (ProjectiveSpace (TOP-REAL 3)) st (homography N) . P1 = (homography N) . P2 holds

P1 = P2

let P1, P2 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( (homography N) . P1 = (homography N) . P2 implies P1 = P2 )

assume A1: (homography N) . P1 = (homography N) . P2 ; :: thesis: P1 = P2

P1 = (homography (N ~)) . ((homography N) . P1) by Th16

.= P2 by A1, Th16 ;

hence P1 = P2 ; :: thesis: verum

P1 = P2

let P1, P2 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( (homography N) . P1 = (homography N) . P2 implies P1 = P2 )

assume A1: (homography N) . P1 = (homography N) . P2 ; :: thesis: P1 = P2

P1 = (homography (N ~)) . ((homography N) . P1) by Th16

.= P2 by A1, Th16 ;

hence P1 = P2 ; :: thesis: verum