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

( (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