let N be invertible Matrix of 3,F_Real; :: thesis: 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 absolute
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
(homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]|
let h be Element of SubGroupK-isometry; :: thesis: for n11, n12, n13, n21, n22, n23, n31, n32, n33 being Element of F_Real
for P being Element of absolute
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
(homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]|
let n11, n12, n13, n21, n22, n23, n31, n32, n33 be Element of F_Real; :: thesis: for P being Element of absolute
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
(homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]|
let P be Element of absolute ; :: thesis: 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
(homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]|
let u be non zero Element of (TOP-REAL 3); :: thesis: ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> & P = Dir u & u . 3 = 1 implies (homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]| )
assume that
A1: ( h = homography N & N = <*<*n11,n12,n13*>,<*n21,n22,n23*>,<*n31,n32,n33*>*> ) and
A2: ( P = Dir u & u . 3 = 1 ) ; :: thesis: (homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]|
reconsider Q = (homography N) . P as Element of absolute by A1, BKMODEL3:35;
consider v being non zero Element of (TOP-REAL 3) such that
A3: ( Q = Dir v & v . 3 = 1 & absolute_to_REAL2 Q = |[(v . 1),(v . 2)]| ) by BKMODEL1:def 8;

now :: thesis: ( v `1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v `2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v `3 = 1 & (homography N) . P = Dir |[(v `1),(v `2),(v `3)]| )

( ((n31 * (u . 1)) + (n32 * (u . 2))) + n33 <> 0 & v . 1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v . 2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) ) by A3, A2, A1, Th21;
hence ( v `1 = (((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v `2 = (((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33) & v `3 = 1 ) by A3, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3; :: thesis: (homography N) . P = Dir |[(v `1),(v `2),(v `3)]|
thus (homography N) . P = Dir |[(v `1),(v `2),(v `3)]| by A3, EUCLID_5:3; :: thesis: verum

end;

hence (homography N) . P = Dir |[((((n11 * (u . 1)) + (n12 * (u . 2))) + n13) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),((((n21 * (u . 1)) + (n22 * (u . 2))) + n23) / (((n31 * (u . 1)) + (n32 * (u . 2))) + n33)),1]| ; :: thesis: verum