theorem Th16: :: ANPROJ_9:15

for N being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( (homography N) . ((homography (N ~)) . P) = P & (homography (N ~)) . ((homography N) . P) = P )