for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds (line_homography (1. (F_Real,3))) . l = l