theorem Th36: :: BKMODEL4:42

for h being Element of SubGroupK-isometry
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 u2 being Element of (TOP-REAL 2) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in inside_of_circle (0,0,1) holds
((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0