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