let N be invertible Matrix of 3,F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3)) holds
( (homography N) . ((homography (N ~)) . P) = P & (homography (N ~)) . ((homography N) . P) = P )
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: ( (homography N) . ((homography (N ~)) . P) = P & (homography (N ~)) . ((homography N) . P) = P )
A1: N ~ is_reverse_of N by MATRIX_6:def 4;
thus (homography N) . ((homography (N ~)) . P) = (homography (N * (N ~))) . P by Th14
.= (homography (1. (F_Real,3))) . P by A1, MATRIX_6:def 2
.= P by Th15 ; :: thesis: (homography (N ~)) . ((homography N) . P) = P
thus (homography (N ~)) . ((homography N) . P) = (homography ((N ~) * N)) . P by Th14
.= (homography (1. (F_Real,3))) . P by A1, MATRIX_6:def 2
.= P by Th15 ; :: thesis: verum