let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: (homography (1. (F_Real,3))) . P = P
consider u, v being Element of (TOP-REAL 3), uf being FinSequence of F_Real, p being FinSequence of 1 -tuples_on REAL such that
A1: P = Dir u and
not u is zero and
A3: u = uf and
A4: p = (1. (F_Real,3)) * uf and
A5: v = M2F p and
not v is zero and
A7: (homography (1. (F_Real,3))) . P = Dir v by ANPROJ_8:def 4;
u in TOP-REAL 3 ;
then A8: uf in REAL 3 by A3, EUCLID:22;
then A9: len uf = 3 by EUCLID_8:50;
A10: (1. (F_Real,3)) * uf = (1. (F_Real,3)) * (<*uf*> @) by LAPLACE:def 9
.= <*uf*> @ by A8, EUCLID_8:50, ANPROJ_8:99 ;
reconsider ur = uf as FinSequence of REAL ;
p = F2M ur by A4, A8, A10, EUCLID_8:50, ANPROJ_8:88;
hence (homography (1. (F_Real,3))) . P = P by A1, A3, A5, A7, A9, ANPROJ_8:86; :: thesis: verum