let P be Element of BK_model ; :: thesis: for h being Element of SubGroupK-isometry

for N being invertible Matrix of 3,F_Real st h = homography N holds

ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 )

let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N holds

ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 )

let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N implies ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 ) )

assume h = homography N ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 )

then reconsider hP = (homography N) . P as Element of BK_model by Th31;

ex u being non zero Element of (TOP-REAL 3) st

( Dir u = hP & u . 3 = 1 & BK_to_REAL2 hP = |[(u . 1),(u . 2)]| ) by BKMODEL2:def 2;

hence ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 ) ; :: thesis: verum

for N being invertible Matrix of 3,F_Real st h = homography N holds

ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 )

let h be Element of SubGroupK-isometry; :: thesis: for N being invertible Matrix of 3,F_Real st h = homography N holds

ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 )

let N be invertible Matrix of 3,F_Real; :: thesis: ( h = homography N implies ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 ) )

assume h = homography N ; :: thesis: ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 )

then reconsider hP = (homography N) . P as Element of BK_model by Th31;

ex u being non zero Element of (TOP-REAL 3) st

( Dir u = hP & u . 3 = 1 & BK_to_REAL2 hP = |[(u . 1),(u . 2)]| ) by BKMODEL2:def 2;

hence ex u being non zero Element of (TOP-REAL 3) st

( (homography N) . P = Dir u & u . 3 = 1 ) ; :: thesis: verum