let N1 be invertible Matrix of 3,F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3))
for a being non zero Element of F_Real holds (homography (a * N1)) . P = (homography N1) . P
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for a being non zero Element of F_Real holds (homography (a * N1)) . P = (homography N1) . P
let a be non zero Element of F_Real; :: thesis: (homography (a * N1)) . P = (homography N1) . P
set M = a * (1. (F_Real,3));
thus (homography (a * N1)) . P = (homography ((a * (1. (F_Real,3))) * N1)) . P by Th02
.= (homography (a * (1. (F_Real,3)))) . ((homography N1) . P) by Th14
.= (homography N1) . P by Th17 ; :: thesis: verum