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

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