let P be Point of (ProjectiveSpace (TOP-REAL 3)); (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; verum