let h be Element of SubGroupK-isometry; :: thesis: 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
let N be invertible Matrix of 3,F_Real; :: thesis: 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
let n11, n12, n13, n21, n22, n23, n31, n32, n33 be Element of F_Real; :: thesis: 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
let u2 be Element of (TOP-REAL 2); :: thesis: ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & u2 in inside_of_circle (0,0,1) implies ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0 )
assume that
A1: h = homography N and
A2: N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> and
A3: u2 in inside_of_circle (0,0,1) ; :: thesis: ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0
reconsider uic = u2 as Element of inside_of_circle (0,0,1) by A3;
consider Q being Element of (TOP-REAL 2) such that
A4: ( Q = uic & REAL2_to_BK uic = Dir |[(Q `1),(Q `2),1]| ) by BKMODEL2:def 3;
reconsider P = REAL2_to_BK uic as Element of BK_model ;
reconsider v = |[(Q `1),(Q `2),1]| as non zero Element of (TOP-REAL 3) ;
A5: v . 1 = v `1 by EUCLID_5:def 1
.= u2 . 1 by A4, EUCLID_5:2 ;
A6: v . 2 = v `2 by EUCLID_5:def 2
.= u2 . 2 by A4, EUCLID_5:2 ;

now :: thesis: ( P = Dir v & v . 3 = 1 )

thus P = Dir v by A4; :: thesis: v . 3 = 1
thus v . 3 = v `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ; :: thesis: verum

end;

hence ((n31 * (u2 . 1)) + (n32 * (u2 . 2))) + n33 <> 0 by A5, A6, A1, A2, Th20; :: thesis: verum