theorem Th17: :: ANPROJ_9:17

for N being invertible Matrix of 3,F_Real
for P being Point of (ProjectiveSpace (TOP-REAL 3))
for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds
(homography N) . P = P