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

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