let N be invertible Matrix of 3,F_Real; :: thesis: for l1, l2 being Element of the Lines of (IncProjSp_of real_projective_plane) st (line_homography N) . l1 = (line_homography N) . l2 holds
l1 = l2
let l1, l2 be Element of the Lines of (IncProjSp_of real_projective_plane); :: thesis: ( (line_homography N) . l1 = (line_homography N) . l2 implies l1 = l2 )
assume (line_homography N) . l1 = (line_homography N) . l2 ; :: thesis: l1 = l2
then l1 = (line_homography (N ~)) . ((line_homography N) . l2) by Th15
.= l2 by Th15 ;
hence l1 = l2 ; :: thesis: verum