theorem Th18: :: BKMODEL4:28

for N being invertible Matrix of 3,F_Real
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P, Q being Point of (ProjectiveSpace (TOP-REAL 3))
for u, v being non zero Element of (TOP-REAL 3) st N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & Q = Dir v & Q = (homography N) . P & u . 3 = 1 holds
ex a being non zero Real st
( v . 1 = a * (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) & v . 2 = a * (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) & v . 3 = a * (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) )