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) holds
( P in l iff (homography N) . P in (line_homography N) . l )
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for l being LINE of (IncProjSp_of real_projective_plane) holds
( P in l iff (homography N) . P in (line_homography N) . l )
let l be LINE of (IncProjSp_of real_projective_plane); :: thesis: ( P in l iff (homography N) . P in (line_homography N) . l )

hereby :: thesis: ( (homography N) . P in (line_homography N) . l implies P in l )

assume A1: P in l ; :: thesis: (homography N) . P in (line_homography N) . l
reconsider P9 = P as POINT of (IncProjSp_of real_projective_plane) by INCPROJ:3;
l is LINE of real_projective_plane by INCPROJ:4;
then A2: P9 on l by A1, INCPROJ:5;
(line_homography N) . l = { ((homography N) . P) where P is POINT of (IncProjSp_of real_projective_plane) : P on l } by Def02;
hence (homography N) . P in (line_homography N) . l by A2; :: thesis: verum

end;

assume (homography N) . P in (line_homography N) . l ; :: thesis: P in l
then P in (line_homography (N ~)) . ((line_homography N) . l) by Th19;
hence P in l by Th15; :: thesis: verum