let N be invertible Matrix of 3,F_Real; :: thesis: for l being Element of the Lines of (IncProjSp_of real_projective_plane) holds
( (line_homography N) . ((line_homography (N ~)) . l) = l & (line_homography (N ~)) . ((line_homography N) . l) = l )
let l be Element of the Lines of (IncProjSp_of real_projective_plane); :: thesis: ( (line_homography N) . ((line_homography (N ~)) . l) = l & (line_homography (N ~)) . ((line_homography N) . l) = l )
A1: N ~ is_reverse_of N by MATRIX_6:def 4;
thus (line_homography N) . ((line_homography (N ~)) . l) = (line_homography (N * (N ~))) . l by Th13
.= (line_homography (1. (F_Real,3))) . l by A1, MATRIX_6:def 2
.= l by Th14 ; :: thesis: (line_homography (N ~)) . ((line_homography N) . l) = l
thus (line_homography (N ~)) . ((line_homography N) . l) = (line_homography ((N ~) * N)) . l by Th13
.= (line_homography (1. (F_Real,3))) . l by A1, MATRIX_6:def 2
.= l by Th14 ; :: thesis: verum