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 (homography N) . P in l holds
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) st (homography N) . P in l holds
P in (line_homography (N ~)) . l
let l be LINE of (IncProjSp_of real_projective_plane); :: thesis: ( (homography N) . P in l implies P in (line_homography (N ~)) . l )
assume A1: (homography N) . P in l ; :: thesis: P in (line_homography (N ~)) . l
reconsider P9 = (homography N) . 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;
then (homography (N ~)) . P9 in (line_homography (N ~)) . l by A2;
hence P in (line_homography (N ~)) . l by ANPROJ_9:15; :: thesis: verum