let N be invertible Matrix of 3,F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3))
for l being LINE of (IncProjSp_of real_projective_plane) st P in (line_homography N) . l holds
(homography (N ~)) . P in l
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for l being LINE of (IncProjSp_of real_projective_plane) st P in (line_homography N) . l holds
(homography (N ~)) . P in l
let l be LINE of (IncProjSp_of real_projective_plane); :: thesis: ( P in (line_homography N) . l implies (homography (N ~)) . P in l )
assume P in (line_homography N) . l ; :: thesis: (homography (N ~)) . P in l
then P in { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by Def02;
then consider P9 being POINT of (IncProjSp_of real_projective_plane) such that
A1: P = (homography N) . P9 and
A2: P9 on l ;
P9 is Element of real_projective_plane by INCPROJ:3;
then A3: (homography (N ~)) . P = P9 by A1, ANPROJ_9:15;
l is LINE of real_projective_plane by INCPROJ:4;
hence (homography (N ~)) . P in l by A2, A3, INCPROJ:5; :: thesis: verum