let N be invertible Matrix of 3,F_Real; for h being Element of SubGroupK-isometry
for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model
for u being non zero Element of (TOP-REAL 3) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 holds
((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0
let h be Element of SubGroupK-isometry; for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of BK_model
for u being non zero Element of (TOP-REAL 3) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 holds
((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0
let n11, n12, n13, n21, n22, n23, n31, n32, n33 be Element of F_Real; for P being Element of BK_model
for u being non zero Element of (TOP-REAL 3) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 holds
((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0
let P be Element of BK_model ; for u being non zero Element of (TOP-REAL 3) st h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 holds
((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0
let u be non zero Element of (TOP-REAL 3); ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 implies ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 )
assume A1:
( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 )
; ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0
reconsider Q = (homography N) . P as Point of (ProjectiveSpace (TOP-REAL 3)) ;
reconsider Q = (homography N) . P as Element of BK_model by A1, BKMODEL3:36;
ex v being non zero Element of (TOP-REAL 3) st
( Q = Dir v & v . 3 = 1 & BK_to_REAL2 Q = |[(v . 1),(v . 2)]| )
by BKMODEL2:def 2;
hence
((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0
by A1, Th19; verum