let P1, P2, P3 be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
assume A1: not P1,P2,P3 are_collinear ; :: thesis:
consider u1 being Element of (TOP-REAL 3) such that
A2: not u1 is zero and
A3: P1 = Dir u1 by ANPROJ_1:26;
consider u2 being Element of (TOP-REAL 3) such that
A4: not u2 is zero and
A5: P2 = Dir u2 by ANPROJ_1:26;
consider u3 being Element of (TOP-REAL 3) such that
A6: not u3 is zero and
A7: P3 = Dir u3 by ANPROJ_1:26;
A8: |{u1,u2,u3}| <> 0 by ANPROJ_8:43, A1, A2, A3, A4, A5, A6, A7, ANPROJ_2:23;
reconsider pf = u1, qf = u2, rf = u3 as FinSequence of F_Real by RVSUM_1:145;
consider N being Matrix of 3,F_Real such that
A9: N is invertible and
A10: N * pf = F2M <e1> and
A11: N * qf = F2M <e2> and
A12: N * rf = F2M <e3> by A8, ANPROJ_8:94;
reconsider N = N as invertible Matrix of 3,F_Real by A9;
A13: ( len <e1> = 3 & len <e2> = 3 & len <e3> = 3 ) by EUCLID_8:50;
take N ; :: thesis:
thus (homography N) . P1 = Dir100 :: thesis:

proof

consider nu1, nv1 being Element of (TOP-REAL 3), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that
A14: P1 = Dir nu1 and
A15: not nu1 is zero and
A16: nu1 = u1f and
A17: p1 = N * u1f and
A18: nv1 = M2F p1 and
A19: not nv1 is zero and
A20: (homography N) . P1 = Dir nv1 by ANPROJ_8:def 4;
are_Prop u1,nu1 by A2, A3, A14, A15, ANPROJ_1:22;
then consider a being Real such that
A21: a <> 0 and
A22: u1 = a * nu1 by ANPROJ_1:1;
reconsider b = 1 / a as Real ;
nu1 in TOP-REAL 3 ;
then A23: nu1 in REAL 3 by EUCLID:22;
width <*u1f*> = len nu1 by A16, ANPROJ_8:75
.= 3 by A23, EUCLID_8:50 ;
then A24: len (<*u1f*> @) = width <*u1f*> by MATRIX_0:29
.= len nu1 by ANPROJ_8:75, A16
.= 3 by A23, EUCLID_8:50 ;
A25: width N = len (<*u1f*> @) by MATRIX_0:24, A24;
A26: len (N * u1f) = len (N * (<*u1f*> @)) by LAPLACE:def 9
.= len N by A25, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
len <e1> = 3 by EUCLID_8:def 1, FINSEQ_1:45;
then A27: F2M <e1> = <*<*(<e1> . 1)*>,<*(<e1> . 2)*>,<*(<e1> . 3)*>*> by ANPROJ_8:def 1;
reconsider s1 = u1f . 1, s2 = u1f . 2, s3 = u1f . 3 as Element of F_Real by XREAL_0:def 1;
reconsider t1 = u1 . 1, t2 = u1 . 2, t3 = u1 . 3 as Element of F_Real by XREAL_0:def 1;
A28: ( (N * pf) . 1 = <*(<e1> . 1)*> & (N * pf) . 2 = <*(<e1> . 2)*> & (N * pf) . 3 = <*(<e1> . 3)*> ) by A10, A27;
A29: ((N * pf) . 1) . 1 = |[1,0,0]| . 1 by A28, EUCLID_8:def 1
.= |[1,0,0]| `1 by EUCLID_5:def 1
.= 1 by EUCLID_5:2 ;
A30: ((N * pf) . 2) . 1 = |[1,0,0]| . 2 by A28, EUCLID_8:def 1
.= |[1,0,0]| `2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2 ;
A31: ((N * pf) . 3) . 1 = |[1,0,0]| . 3 by A28, EUCLID_8:def 1
.= |[1,0,0]| `3 by EUCLID_5:def 3
.= 0 by EUCLID_5:2 ;
( p1 . 1 = <*((N * (<*u1f*> @)) * (1,1))*> & p1 . 2 = <*((N * (<*u1f*> @)) * (2,1))*> & p1 . 3 = <*((N * (<*u1f*> @)) * (3,1))*> ) by A16, A17, FINSEQ_1:1, Lem02;
then reconsider p111 = (p1 . 1) . 1, p121 = (p1 . 2) . 1, p131 = (p1 . 3) . 1 as Real ;
A32: ( p111 = b * ((Line (N,1)) "*" pf) & p121 = b * ((Line (N,2)) "*" pf) & p131 = b * ((Line (N,3)) "*" pf) ) by FINSEQ_1:1, A16, A17, A21, A22, Lem04;
A33: a * p1 = N * pf

proof

consider pp1, pp2, pp3 being Real such that
A34: pp1 = (p1 . 1) . 1 and
A35: pp2 = (p1 . 2) . 1 and
A36: pp3 = (p1 . 3) . 1 and
A37: a * p1 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*> by A17, A26, ANPROJ_8:def 3;

now :: thesis:

thus len (N * pf) = 3 by A10, A13, ANPROJ_8:78; :: thesis:
thus (N * pf) . 1 = <*(a * pp1)*> :: thesis:

proof

(Line (N,1)) "*" pf = ((N * pf) . 1) . 1 by FINSEQ_1:1, Lem05;
then ( len ((N * pf) . 1) = 1 & ((N * pf) . 1) . 1 = a * p111 ) by A28, FINSEQ_1:40, A29, A32, A21, XCMPLX_1:87;
hence (N * pf) . 1 = <*(a * pp1)*> by A34, FINSEQ_1:40; :: thesis:

end;

thus (N * pf) . 2 = <*(a * pp2)*> :: thesis:

proof

(Line (N,2)) "*" pf = ((N * pf) . 2) . 1 by FINSEQ_1:1, Lem05;
hence (N * pf) . 2 = <*(a * pp2)*> by A35, A28, A30, A32; :: thesis:

end;

(Line (N,3)) "*" pf = ((N * pf) . 3) . 1 by FINSEQ_1:1, Lem05;
hence (N * pf) . 3 = <*(a * pp3)*> by A36, A28, A32, A31; :: thesis:

end;

hence a * p1 = N * pf by A37, FINSEQ_1:45; :: thesis:

end;

len <e1> = 3 by EUCLID_8:50;
then A38: <e1> = M2F (F2M <e1>) by ANPROJ_8:86
.= a * nv1 by A18, A33, A10, A26, A17, ANPROJ_8:83 ;
( not nv1 is zero & not a * nv1 is zero & are_Prop nv1,a * nv1 ) by A19, A21, Th04, ANPROJ_1:1;
hence (homography N) . P1 = Dir100 by A38, EUCLID_8:def 1, ANPROJ_1:22, A20; :: thesis:

end;

thus (homography N) . P2 = Dir010 :: thesis:

proof

consider nu2, nv2 being Element of (TOP-REAL 3), u2f being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that
A39: P2 = Dir nu2 and
A40: not nu2 is zero and
A41: nu2 = u2f and
A42: p2 = N * u2f and
A43: nv2 = M2F p2 and
A44: not nv2 is zero and
A45: (homography N) . P2 = Dir nv2 by ANPROJ_8:def 4;
are_Prop u2,nu2 by A4, A5, A39, A40, ANPROJ_1:22;
then consider a being Real such that
A46: a <> 0 and
A47: u2 = a * nu2 by ANPROJ_1:1;
reconsider b = 1 / a as Real ;
nu2 in TOP-REAL 3 ;
then A48: nu2 in REAL 3 by EUCLID:22;
width <*u2f*> = len nu2 by A41, ANPROJ_8:75
.= 3 by A48, EUCLID_8:50 ;
then A49: len (<*u2f*> @) = width <*u2f*> by MATRIX_0:29
.= len nu2 by ANPROJ_8:75, A41
.= 3 by A48, EUCLID_8:50 ;
A50: width N = len (<*u2f*> @) by MATRIX_0:24, A49;
A51: len (N * u2f) = len (N * (<*u2f*> @)) by LAPLACE:def 9
.= len N by A50, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
len <e2> = 3 by EUCLID_8:def 2, FINSEQ_1:45;
then A52: F2M <e2> = <*<*(<e2> . 1)*>,<*(<e2> . 2)*>,<*(<e2> . 3)*>*> by ANPROJ_8:def 1;
reconsider s1 = u2f . 1, s2 = u2f . 2, s3 = u2f . 3 as Element of F_Real by XREAL_0:def 1;
reconsider t1 = u2 . 1, t2 = u2 . 2, t3 = u2 . 3 as Element of F_Real by XREAL_0:def 1;
A53: ( (N * qf) . 1 = <*(<e2> . 1)*> & (N * qf) . 2 = <*(<e2> . 2)*> & (N * qf) . 3 = <*(<e2> . 3)*> ) by A11, A52;
A54: ((N * qf) . 1) . 1 = |[0,1,0]| . 1 by A53, EUCLID_8:def 2
.= |[0,1,0]| `1 by EUCLID_5:def 1
.= 0 by EUCLID_5:2 ;
A55: ((N * qf) . 2) . 1 = |[0,1,0]| . 2 by A53, EUCLID_8:def 2
.= |[0,1,0]| `2 by EUCLID_5:def 2
.= 1 by EUCLID_5:2 ;
A56: ((N * qf) . 3) . 1 = |[0,1,0]| . 3 by A53, EUCLID_8:def 2
.= |[0,1,0]| `3 by EUCLID_5:def 3
.= 0 by EUCLID_5:2 ;
( p2 . 1 = <*((N * (<*u2f*> @)) * (1,1))*> & p2 . 2 = <*((N * (<*u2f*> @)) * (2,1))*> & p2 . 3 = <*((N * (<*u2f*> @)) * (3,1))*> ) by A41, A42, FINSEQ_1:1, Lem02;
then reconsider p211 = (p2 . 1) . 1, p221 = (p2 . 2) . 1, p231 = (p2 . 3) . 1 as Real ;
A57: ( p211 = b * ((Line (N,1)) "*" qf) & p221 = b * ((Line (N,2)) "*" qf) & p231 = b * ((Line (N,3)) "*" qf) ) by FINSEQ_1:1, A41, A42, A46, A47, Lem04;
A58: a * p2 = N * qf

proof

consider pp1, pp2, pp3 being Real such that
A59: pp1 = (p2 . 1) . 1 and
A60: pp2 = (p2 . 2) . 1 and
A61: pp3 = (p2 . 3) . 1 and
A62: a * p2 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*> by A42, A51, ANPROJ_8:def 3;

now :: thesis:

thus len (N * qf) = 3 by A11, A13, ANPROJ_8:78; :: thesis:
(Line (N,1)) "*" qf = ((N * qf) . 1) . 1 by FINSEQ_1:1, Lem05;
hence (N * qf) . 1 = <*(a * pp1)*> by A59, A53, A57, A54; :: thesis:
thus (N * qf) . 2 = <*(a * pp2)*> :: thesis:

proof

(Line (N,2)) "*" qf = ((N * qf) . 2) . 1 by FINSEQ_1:1, Lem05;
then ( len ((N * qf) . 2) = 1 & ((N * qf) . 2) . 1 = a * p221 ) by A53, FINSEQ_1:40, A55, A57, A46, XCMPLX_1:87;
hence (N * qf) . 2 = <*(a * pp2)*> by A60, FINSEQ_1:40; :: thesis:

end;

(Line (N,3)) "*" qf = ((N * qf) . 3) . 1 by FINSEQ_1:1, Lem05;
hence (N * qf) . 3 = <*(a * pp3)*> by A61, A53, A57, A56; :: thesis:

end;

hence a * p2 = N * qf by A62, FINSEQ_1:45; :: thesis:

end;

len <e2> = 3 by EUCLID_8:50;
then A63: <e2> = M2F (F2M <e2>) by ANPROJ_8:86
.= a * nv2 by A43, A58, A11, A51, A42, ANPROJ_8:83 ;
( not nv2 is zero & not a * nv2 is zero & are_Prop nv2,a * nv2 ) by A44, A46, Th04, ANPROJ_1:1;
hence (homography N) . P2 = Dir010 by A63, EUCLID_8:def 2, ANPROJ_1:22, A45; :: thesis:

end;

thus (homography N) . P3 = Dir001 :: thesis:

proof

consider nu3, nv3 being Element of (TOP-REAL 3), u3f being FinSequence of F_Real, p3 being FinSequence of 1 -tuples_on REAL such that
A64: P3 = Dir nu3 and
A65: not nu3 is zero and
A66: nu3 = u3f and
A67: p3 = N * u3f and
A68: nv3 = M2F p3 and
A69: not nv3 is zero and
A70: (homography N) . P3 = Dir nv3 by ANPROJ_8:def 4;
are_Prop u3,nu3 by A6, A7, A64, A65, ANPROJ_1:22;
then consider a being Real such that
A71: a <> 0 and
A72: u3 = a * nu3 by ANPROJ_1:1;
reconsider b = 1 / a as Real ;
nu3 in TOP-REAL 3 ;
then A73: nu3 in REAL 3 by EUCLID:22;
width <*u3f*> = len nu3 by A66, ANPROJ_8:75
.= 3 by A73, EUCLID_8:50 ;
then A74: len (<*u3f*> @) = width <*u3f*> by MATRIX_0:29
.= len nu3 by ANPROJ_8:75, A66
.= 3 by A73, EUCLID_8:50 ;
A75: width N = len (<*u3f*> @) by MATRIX_0:24, A74;
A76: len (N * u3f) = len (N * (<*u3f*> @)) by LAPLACE:def 9
.= len N by A75, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
len <e3> = 3 by EUCLID_8:def 3, FINSEQ_1:45;
then A77: F2M <e3> = <*<*(<e3> . 1)*>,<*(<e3> . 2)*>,<*(<e3> . 3)*>*> by ANPROJ_8:def 1;
reconsider s1 = u3f . 1, s2 = u3f . 2, s3 = u3f . 3 as Element of F_Real by XREAL_0:def 1;
reconsider t1 = u3 . 1, t2 = u3 . 2, t3 = u3 . 3 as Element of F_Real by XREAL_0:def 1;
A78: ( (N * rf) . 1 = <*(<e3> . 1)*> & (N * rf) . 2 = <*(<e3> . 2)*> & (N * rf) . 3 = <*(<e3> . 3)*> ) by A12, A77;
A79: ((N * rf) . 1) . 1 = |[0,0,1]| . 1 by A78, EUCLID_8:def 3
.= |[0,0,1]| `1 by EUCLID_5:def 1
.= 0 by EUCLID_5:2 ;
A80: ((N * rf) . 2) . 1 = |[0,0,1]| . 2 by A78, EUCLID_8:def 3
.= |[0,0,1]| `2 by EUCLID_5:def 2
.= 0 by EUCLID_5:2 ;
A81: ((N * rf) . 3) . 1 = |[0,0,1]| . 3 by A78, EUCLID_8:def 3
.= |[0,0,1]| `3 by EUCLID_5:def 3
.= 1 by EUCLID_5:2 ;
( p3 . 1 = <*((N * (<*u3f*> @)) * (1,1))*> & p3 . 2 = <*((N * (<*u3f*> @)) * (2,1))*> & p3 . 3 = <*((N * (<*u3f*> @)) * (3,1))*> ) by A66, A67, FINSEQ_1:1, Lem02;
then reconsider p311 = (p3 . 1) . 1, p321 = (p3 . 2) . 1, p331 = (p3 . 3) . 1 as Real ;
A82: ( p311 = b * ((Line (N,1)) "*" rf) & p321 = b * ((Line (N,2)) "*" rf) & p331 = b * ((Line (N,3)) "*" rf) ) by FINSEQ_1:1, A66, A67, A71, A72, Lem04;
A83: a * p3 = N * rf

proof

consider pp1, pp2, pp3 being Real such that
A84: pp1 = (p3 . 1) . 1 and
A85: pp2 = (p3 . 2) . 1 and
A86: pp3 = (p3 . 3) . 1 and
A87: a * p3 = <*<*(a * pp1)*>,<*(a * pp2)*>,<*(a * pp3)*>*> by A67, A76, ANPROJ_8:def 3;

now :: thesis:

thus len (N * rf) = 3 by A12, A13, ANPROJ_8:78; :: thesis:
(Line (N,1)) "*" rf = ((N * rf) . 1) . 1 by FINSEQ_1:1, Lem05;
hence (N * rf) . 1 = <*(a * pp1)*> by A84, A78, A82, A79; :: thesis:
(Line (N,2)) "*" rf = ((N * rf) . 2) . 1 by FINSEQ_1:1, Lem05;
hence (N * rf) . 2 = <*(a * pp2)*> by A85, A78, A82, A80; :: thesis:
thus (N * rf) . 3 = <*(a * pp3)*> :: thesis:

proof

(Line (N,3)) "*" rf = ((N * rf) . 3) . 1 by FINSEQ_1:1, Lem05;
then ( len ((N * rf) . 3) = 1 & ((N * rf) . 3) . 1 = a * p331 ) by A78, FINSEQ_1:40, A81, A82, A71, XCMPLX_1:87;
hence (N * rf) . 3 = <*(a * pp3)*> by A86, FINSEQ_1:40; :: thesis:

end;

hence a * p3 = N * rf by A87, FINSEQ_1:45; :: thesis:

end;

len <e3> = 3 by EUCLID_8:50;
then A88: <e3> = M2F (F2M <e3>) by ANPROJ_8:86
.= a * nv3 by A68, A83, A12, A76, A67, ANPROJ_8:83 ;
( not nv3 is zero & not a * nv3 is zero & are_Prop nv3,a * nv3 ) by A69, A71, Th04, ANPROJ_1:1;
hence (homography N) . P3 = Dir001 by A88, EUCLID_8:def 3, ANPROJ_1:22, A70; :: thesis:

end;