for N being invertible Matrix of 3,F_Real
for p, q, r, s, t, u, np, nq, nr, ns being Element of real_projective_plane st p <> q & r <> s & np <> nq & nr <> ns & p,q,t are_collinear & r,s,t are_collinear & np = (homography N) . p & nq = (homography N) . q & nr = (homography N) . r & ns = (homography N) . s & np,nq,u are_collinear & nr,ns,u are_collinear & not p,q,r are_collinear holds
u = (homography N) . t