for N being invertible Matrix of 3,F_Real
for NR being Matrix of 3,REAL
for P, Q being Element of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3)
for vfr, ufr being FinSequence of REAL st P = Dir u & Q = Dir v & u = ufr & v = vfr & N = NR & NR * ufr = vfr holds
(homography N) . P = Q