let a, b, c, ia, ib, ic be non zero Element of F_Real; :: thesis: for P being Point of (ProjectiveSpace (TOP-REAL 3))
for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds
(homography N) . P = Dir |[1,1,1]|
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis: for N being invertible Matrix of 3,F_Real st P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> holds
(homography N) . P = Dir |[1,1,1]|
let N be invertible Matrix of 3,F_Real; :: thesis: ( P = Dir |[a,b,c]| & ia = 1 / a & ib = 1 / b & ic = 1 / c & N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> implies (homography N) . P = Dir |[1,1,1]| )
assume that
A1: P = Dir |[a,b,c]| and
A2: ia = 1 / a and
A3: ib = 1 / b and
A4: ic = 1 / c and
A5: N = <*<*ia,0,0*>,<*0,ib,0*>,<*0,0,ic*>*> ; :: thesis: (homography N) . P = Dir |[1,1,1]|
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
A15: P = Dir u and
A16: not u is zero and
A17: u = uf and
A18: p = N * uf and
A19: v = M2F p and
A20: not v is zero and
A21: (homography N) . P = Dir v by ANPROJ_8:def 4;
not |[a,b,c]| is zero

proof

assume |[a,b,c]| is zero ; :: thesis: contradiction
then ( a is zero & b is zero & c is zero ) by EUCLID_5:4, FINSEQ_1:78;
hence contradiction ; :: thesis: verum

end;

then are_Prop u,|[a,b,c]| by A1, A15, A16, ANPROJ_1:22;
then consider d being Real such that
A22: d <> 0 and
A23: u = d * |[a,b,c]| by ANPROJ_1:1;
A24: u = <*(d * a),(d * b),(d * c)*> by A23, EUCLID_5:8;
A25: ( uf . 1 = d * a & uf . 2 = d * b & uf . 3 = d * c ) by A24, A17;
u in TOP-REAL 3 ;
then u in REAL 3 by EUCLID:22;
then A26: <*uf*> @ = <*<*(d * a)*>,<*(d * b)*>,<*(d * c)*>*> by A25, A17, EUCLID_8:50, ANPROJ_8:77;
reconsider Mu = <*uf*> @ as Matrix of 3,1,F_Real by A26, ANPROJ_8:4;
reconsider z = 0 , da = d * a, db = d * b, dc = d * c as Element of F_Real by XREAL_0:def 1;
A27: p = N * Mu by A18, LAPLACE:def 9
.= <*<*(((ia * da) + (z * db)) + (z * dc))*>,<*(((z * da) + (ib * db)) + (z * dc))*>,<*(((z * da) + (z * db)) + (ic * dc))*>*> by A26, A5, Th08
.= <*<*(ia * da)*>,<*(ib * db)*>,<*(ic * dc)*>*> ;
A28: v = |[(ia * da),(ib * db),(ic * dc)]|

proof

A29: ( <*(ia * da)*> . 1 = ia * da & <*(ib * db)*> . 1 = ib * db & <*(ic * dc)*> . 1 = ic * dc ) ;
A30: ( p . 1 = <*(ia * da)*> & p . 2 = <*(ib * db)*> & p . 3 = <*(ic * dc)*> ) by A27;
len p = 3 by A27, FINSEQ_1:45;
hence v = |[(ia * da),(ib * db),(ic * dc)]| by A29, A30, A19, ANPROJ_8:def 2; :: thesis: verum

end;

A31: ( not a is zero & not b is zero & not c is zero ) ;

now :: thesis: ( ia * da = d & ib * db = d & ic * dc = d )

thus ia * da = ((1 / a) * a) * d by A2
.= 1 * d by A31, XCMPLX_1:106
.= d ; :: thesis: ( ib * db = d & ic * dc = d )
thus ib * db = ((1 / b) * b) * d by A3
.= 1 * d by A31, XCMPLX_1:106
.= d ; :: thesis: ic * dc = d
thus ic * dc = ((1 / c) * c) * d by A4
.= 1 * d by A31, XCMPLX_1:106
.= d ; :: thesis: verum

end;

then v = |[(d * 1),(d * 1),(d * 1)]| by A28
.= d * |[1,1,1]| by EUCLID_5:8 ;
then are_Prop v,|[1,1,1]| by A22, ANPROJ_1:1;
hence (homography N) . P = Dir |[1,1,1]| by Th11, A20, ANPROJ_1:22, A21; :: thesis: verum