:: deftheorem DEF4 defines homography ANPROJ_8:def 4 :
for N being invertible Matrix of 3,F_Real
for b₂ being Function of (ProjectiveSpace (TOP-REAL 3)),(ProjectiveSpace (TOP-REAL 3)) holds
( b₂ = homography N iff for x being Point of (ProjectiveSpace (TOP-REAL 3)) ex u, v being Element of (TOP-REAL 3) ex uf being FinSequence of F_Real ex p being FinSequence of 1 -tuples_on REAL st
( x = Dir u & not u is zero & u = uf & p = N * uf & v = M2F p & not v is zero & b₂ . x = Dir v ) );