let N 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 st a * (1. (F_Real,3)) = N holds
(homography N) . P = P
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for a being non zero Element of F_Real st a * (1. (F_Real,3)) = N holds
(homography N) . P = P
let a be non zero Element of F_Real; :: thesis: ( a * (1. (F_Real,3)) = N implies (homography N) . P = P )
assume A1: a * (1. (F_Real,3)) = N ; :: thesis: (homography N) . P = P
set aN = N;
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
A2: P = Dir u and
A3: not u is zero and
A4: u = uf and
A5: p = N * uf and
A6: v = M2F p and
A7: not v is zero and
A8: (homography N) . P = Dir v by ANPROJ_8:def 4;
u in TOP-REAL 3 ;
then A9: uf in REAL 3 by A4, EUCLID:22;
A10: N * (<*uf*> @) is Matrix of 3,1,F_Real by A4, FINSEQ_3:153, ANPROJ_8:91;
p = N * (<*uf*> @) by A5, LAPLACE:def 9;
then A11: len p = 3 by A10, MATRIX_0:23;
A12: p = N * (<*uf*> @) by A5, LAPLACE:def 9
.= a * (<*uf*> @) by A1, A9, EUCLID_8:50, Lem06 ;
A13: v = <*(((a * (<*uf*> @)) . 1) . 1),(((a * (<*uf*> @)) . 2) . 1),(((a * (<*uf*> @)) . 3) . 1)*> by A6, A12, A11, ANPROJ_8:def 2;

now :: thesis: ( ((a * (<*uf*> @)) . 1) . 1 = a * (u . 1) & ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) & ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) )

(1. (F_Real,3)) * (<*uf*> @) is 3,1 -size by A9, EUCLID_8:50, ANPROJ_8:91;
then A14: <*uf*> @ is 3,1 -size by A9, EUCLID_8:50, ANPROJ_8:99;
A15: ( [1,1] in Indices (<*uf*> @) & [2,1] in Indices (<*uf*> @) & [3,1] in Indices (<*uf*> @) ) by A14, MATRIX_0:23, ANPROJ_8:2;
then A16: ( (a * (<*uf*> @)) * (1,1) = a * ((<*uf*> @) * (1,1)) & (a * (<*uf*> @)) * (2,1) = a * ((<*uf*> @) * (2,1)) & (a * (<*uf*> @)) * (3,1) = a * ((<*uf*> @) * (3,1)) ) by MATRIX_3:def 5;
A17: <*uf*> @ = <*<*(uf . 1)*>,<*(uf . 2)*>,<*(uf . 3)*>*> by A9, EUCLID_8:50, ANPROJ_8:77;
A18: ( len (<*uf*> @) = 3 & width (<*uf*> @) = 1 ) by A14, MATRIX_0:23;
A19: ( len (a * (<*uf*> @)) = len (<*uf*> @) & width (a * (<*uf*> @)) = width (<*uf*> @) ) by MATRIX_3:def 5;
a * (<*uf*> @) is Matrix of 3,1,F_Real by MATRIX_0:20, A19, A18;
then A20: ( [1,1] in Indices (a * (<*uf*> @)) & [2,1] in Indices (a * (<*uf*> @)) & [3,1] in Indices (a * (<*uf*> @)) ) by ANPROJ_8:2, MATRIX_0:23;
(<*uf*> @) * (1,1) = ((<*uf*> @) . 1) . 1 by A15, MATRPROB:14
.= <*(uf . 1)*> . 1 by A17
.= uf . 1 ;
hence ((a * (<*uf*> @)) . 1) . 1 = a * (u . 1) by A4, A20, MATRPROB:14, A16; :: thesis: ( ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) & ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) )
(<*uf*> @) * (2,1) = ((<*uf*> @) . 2) . 1 by A15, MATRPROB:14
.= <*(uf . 2)*> . 1 by A17
.= uf . 2 ;
hence ((a * (<*uf*> @)) . 2) . 1 = a * (u . 2) by A4, A20, MATRPROB:14, A16; :: thesis: ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3)
(<*uf*> @) * (3,1) = ((<*uf*> @) . 3) . 1 by A15, MATRPROB:14
.= <*(uf . 3)*> . 1 by A17
.= uf . 3 ;
hence ((a * (<*uf*> @)) . 3) . 1 = a * (u . 3) by A4, A20, MATRPROB:14, A16; :: thesis: verum

end;

then A21: v = <*(a * (u `1)),(a * (u . 2)),(a * (u . 3))*> by A13, EUCLID_5:def 1
.= <*(a * (u `1)),(a * (u `2)),(a * (u . 3))*> by EUCLID_5:def 2
.= <*(a * (u `1)),(a * (u `2)),(a * (u `3))*> by EUCLID_5:def 3
.= a * |[(u `1),(u `2),(u `3)]| by EUCLID_5:8
.= a * u by EUCLID_5:3 ;
not a is zero ;
then are_Prop v,u by A21, ANPROJ_1:1;
hence (homography N) . P = P by A2, A3, A7, A8, ANPROJ_1:22; :: thesis: verum