let N1, N2 be invertible Matrix of 3,F_Real; :: thesis:
let P be Point of (ProjectiveSpace (TOP-REAL 3)); :: thesis:
consider u12, v12 being Element of (TOP-REAL 3), u12f being FinSequence of F_Real, p12 being FinSequence of 1 -tuples_on REAL such that
A1: P = Dir u12 and
A2: not u12 is zero and
A3: u12 = u12f and
A4: p12 = (N1 * N2) * u12f and
A5: v12 = M2F p12 and
A6: not v12 is zero and
A7: (homography (N1 * N2)) . P = Dir v12 by ANPROJ_8:def 4;
consider u2, v2 being Element of (TOP-REAL 3), u2f being FinSequence of F_Real, p2 being FinSequence of 1 -tuples_on REAL such that
A8: P = Dir u2 and
A9: not u2 is zero and
A10: u2 = u2f and
A11: p2 = N2 * u2f and
A12: v2 = M2F p2 and
A13: not v2 is zero and
A14: (homography N2) . P = Dir v2 by ANPROJ_8:def 4;
consider u1, v1 being Element of (TOP-REAL 3), u1f being FinSequence of F_Real, p1 being FinSequence of 1 -tuples_on REAL such that
A15: (homography N2) . P = Dir u1 and
A16: not u1 is zero and
A17: u1 = u1f and
A18: p1 = N1 * u1f and
A19: v1 = M2F p1 and
A20: not v1 is zero and
A21: (homography N1) . ((homography N2) . P) = Dir v1 by ANPROJ_8:def 4;
are_Prop u12,u2 by A1, A8, A2, A9, ANPROJ_1:22;
then consider a being Real such that
A22: a <> 0 and
A23: u2 = a * u12 by ANPROJ_1:1;
are_Prop v2,u1 by A14, A15, A16, A13, ANPROJ_1:22;
then consider b being Real such that
A24: b <> 0 and
A25: u1 = b * v2 by ANPROJ_1:1;
u1 in TOP-REAL 3 ;
then F2: u1 in REAL 3 by EUCLID:22;
width <*u1f*> = len u1 by A17, ANPROJ_8:75
.= 3 by F2, EUCLID_8:50 ;
then len (<*u1f*> @) = width <*u1f*> by MATRIX_0:29
.= len u1 by ANPROJ_8:75, A17
.= 3 by F2, EUCLID_8:50 ;
then A26: width N1 = len (<*u1f*> @) by MATRIX_0:24;
A27: len (N1 * u1f) = len (N1 * (<*u1f*> @)) by LAPLACE:def 9
.= len N1 by A26, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
A28: v1 = <*((N1 * (<*u1f*> @)) * (1,1)),((N1 * (<*u1f*> @)) * (2,1)),((N1 * (<*u1f*> @)) * (3,1))*>

( p1 . 1 = <*((N1 * (<*u1f*> @)) * (1,1))*> & p1 . 2 = <*((N1 * (<*u1f*> @)) * (2,1))*> & p1 . 3 = <*((N1 * (<*u1f*> @)) * (3,1))*> ) by A17, A18, FINSEQ_1:1, Lem02;
then ( (p1 . 1) . 1 = (N1 * (<*u1f*> @)) * (1,1) & (p1 . 2) . 1 = (N1 * (<*u1f*> @)) * (2,1) & (p1 . 3) . 1 = (N1 * (<*u1f*> @)) * (3,1) ) ;
hence v1 = <*((N1 * (<*u1f*> @)) * (1,1)),((N1 * (<*u1f*> @)) * (2,1)),((N1 * (<*u1f*> @)) * (3,1))*> by A19, A27, A18, ANPROJ_8:def 2; :: thesis:

end;

u2 in TOP-REAL 3 ;
then A29: u2 in REAL 3 by EUCLID:22;
width <*u2f*> = len u2 by A10, ANPROJ_8:75
.= 3 by A29, EUCLID_8:50 ;
then len (<*u2f*> @) = width <*u2f*> by MATRIX_0:29
.= len u2 by ANPROJ_8:75, A10
.= 3 by A29, EUCLID_8:50 ;
then A30: width N2 = len (<*u2f*> @) by MATRIX_0:24;
A31: len (N2 * u2f) = len (N2 * (<*u2f*> @)) by LAPLACE:def 9
.= len N2 by A30, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
A32: v2 = <*((N2 * (<*u2f*> @)) * (1,1)),((N2 * (<*u2f*> @)) * (2,1)),((N2 * (<*u2f*> @)) * (3,1))*>

proof

( p2 . 1 = <*((N2 * (<*u2f*> @)) * (1,1))*> & p2 . 2 = <*((N2 * (<*u2f*> @)) * (2,1))*> & p2 . 3 = <*((N2 * (<*u2f*> @)) * (3,1))*> ) by A10, A11, FINSEQ_1:1, Lem02;
then ( (p2 . 1) . 1 = (N2 * (<*u2f*> @)) * (1,1) & (p2 . 2) . 1 = (N2 * (<*u2f*> @)) * (2,1) & (p2 . 3) . 1 = (N2 * (<*u2f*> @)) * (3,1) ) ;
hence v2 = <*((N2 * (<*u2f*> @)) * (1,1)),((N2 * (<*u2f*> @)) * (2,1)),((N2 * (<*u2f*> @)) * (3,1))*> by A12, A31, A11, ANPROJ_8:def 2; :: thesis:

end;

u12 in TOP-REAL 3 ;
then A33: u12 in REAL 3 by EUCLID:22;
width <*u12f*> = len u12 by A3, ANPROJ_8:75
.= 3 by A33, EUCLID_8:50 ;
then A34: len (<*u12f*> @) = width <*u12f*> by MATRIX_0:29
.= len u12 by ANPROJ_8:75, A3
.= 3 by A33, EUCLID_8:50 ;
A35: width (N1 * N2) = len (<*u12f*> @) by MATRIX_0:24, A34;
A36: len ((N1 * N2) * u12f) = len ((N1 * N2) * (<*u12f*> @)) by LAPLACE:def 9
.= len (N1 * N2) by A35, MATRIX_3:def 4
.= 3 by MATRIX_0:24 ;
A37: v12 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*>

proof

( p12 . 1 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1))*> & p12 . 2 = <*(((N1 * N2) * (<*u12f*> @)) * (2,1))*> & p12 . 3 = <*(((N1 * N2) * (<*u12f*> @)) * (3,1))*> ) by A3, A4, FINSEQ_1:1, Lem02;
then ( (p12 . 1) . 1 = ((N1 * N2) * (<*u12f*> @)) * (1,1) & (p12 . 2) . 1 = ((N1 * N2) * (<*u12f*> @)) * (2,1) & (p12 . 3) . 1 = ((N1 * N2) * (<*u12f*> @)) * (3,1) ) ;
hence v12 = <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*> by A5, A36, A4, ANPROJ_8:def 2; :: thesis:

end;

reconsider v2f = v2 as FinSequence of F_Real by RVSUM_1:145;
reconsider invb = 1 / b as Real ;
A38: v2f = invb * u1

proof

invb * u1 = (invb * b) * v2f by A25, RVSUM_1:49
.= 1 * v2f by A24, XCMPLX_1:106
.= v2f by RVSUM_1:52 ;
hence v2f = invb * u1 ; :: thesis:

end;

( 1 in Seg 3 & 2 in Seg 3 & 3 in Seg 3 ) by FINSEQ_1:1;
then A39: ( (N1 * (<*u1f*> @)) * (1,1) = (1 / invb) * ((Line (N1,1)) "*" v2f) & (N1 * (<*u1f*> @)) * (2,1) = (1 / invb) * ((Line (N1,2)) "*" v2f) & (N1 * (<*u1f*> @)) * (3,1) = (1 / invb) * ((Line (N1,3)) "*" v2f) ) by A24, XCMPLX_1:50, A38, A17, Lem03;
A40: ( len (Line (N1,1)) = width N1 & len (Line (N1,2)) = width N1 & len (Line (N1,3)) = width N1 ) by MATRIX_0:def 7;
width N1 = 3 by MATRIX_0:24;
then ( 1 in Seg (width N1) & 2 in Seg (width N1) & 3 in Seg (width N1) ) by FINSEQ_1:1;
then A41: ( (Line (N1,1)) . 1 = N1 * (1,1) & (Line (N1,1)) . 2 = N1 * (1,2) & (Line (N1,1)) . 3 = N1 * (1,3) & (Line (N1,2)) . 1 = N1 * (2,1) & (Line (N1,2)) . 2 = N1 * (2,2) & (Line (N1,2)) . 3 = N1 * (2,3) & (Line (N1,3)) . 1 = N1 * (3,1) & (Line (N1,3)) . 2 = N1 * (3,2) & (Line (N1,3)) . 3 = N1 * (3,3) ) by MATRIX_0:def 7;
then A42: ( Line (N1,1) = <*(N1 * (1,1)),(N1 * (1,2)),(N1 * (1,3))*> & Line (N1,2) = <*(N1 * (2,1)),(N1 * (2,2)),(N1 * (2,3))*> & Line (N1,3) = <*(N1 * (3,1)),(N1 * (3,2)),(N1 * (3,3))*> ) by A40, MATRIX_0:24, FINSEQ_1:45;
A43: ( len (Line ((N1 * N2),1)) = width (N1 * N2) & len (Line ((N1 * N2),2)) = width (N1 * N2) & len (Line ((N1 * N2),3)) = width (N1 * N2) ) by MATRIX_0:def 7;
width (N1 * N2) = 3 by MATRIX_0:24;
then ( 1 in Seg (width (N1 * N2)) & 2 in Seg (width (N1 * N2)) & 3 in Seg (width (N1 * N2)) ) by FINSEQ_1:1;
then A44: ( (Line ((N1 * N2),1)) . 1 = (N1 * N2) * (1,1) & (Line ((N1 * N2),1)) . 2 = (N1 * N2) * (1,2) & (Line ((N1 * N2),1)) . 3 = (N1 * N2) * (1,3) & (Line ((N1 * N2),2)) . 1 = (N1 * N2) * (2,1) & (Line ((N1 * N2),2)) . 2 = (N1 * N2) * (2,2) & (Line ((N1 * N2),2)) . 3 = (N1 * N2) * (2,3) & (Line ((N1 * N2),3)) . 1 = (N1 * N2) * (3,1) & (Line ((N1 * N2),3)) . 2 = (N1 * N2) * (3,2) & (Line ((N1 * N2),3)) . 3 = (N1 * N2) * (3,3) ) by MATRIX_0:def 7;
reconsider fa = a as Element of F_Real by XREAL_0:def 1;
A45: ( v1 . 1 = (N1 * (<*u1f*> @)) * (1,1) & v1 . 2 = (N1 * (<*u1f*> @)) * (2,1) & v1 . 3 = (N1 * (<*u1f*> @)) * (3,1) ) by A28;
reconsider t1 = v2f . 1, t2 = v2f . 2, t3 = v2f . 3 as Element of F_Real by A32;
len v2f = 3 by A32, FINSEQ_1:45;
then A46: v2f = <*t1,t2,t3*> by FINSEQ_1:45;
N2 * (<*u2f*> @) is Matrix of 3,1,F_Real by A10, FINSEQ_3:153, ANPROJ_8:91;
then A47: ( [1,1] in Indices (N2 * (<*u2f*> @)) & [2,1] in Indices (N2 * (<*u2f*> @)) & [3,1] in Indices (N2 * (<*u2f*> @)) ) by ANPROJ_8:2, MATRIX_0:23;
A48: t1 = (N2 * (<*u2f*> @)) * (1,1) by A32
.= (Line (N2,1)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4
.= (Line (N2,1)) "*" u2f by ANPROJ_8:93 ;
A49: t2 = (N2 * (<*u2f*> @)) * (2,1) by A32
.= (Line (N2,2)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4
.= (Line (N2,2)) "*" u2f by ANPROJ_8:93 ;
A50: t3 = (N2 * (<*u2f*> @)) * (3,1) by A32
.= (Line (N2,3)) "*" (Col ((<*u2f*> @),1)) by A30, A47, MATRIX_3:def 4
.= (Line (N2,3)) "*" u2f by ANPROJ_8:93 ;

now :: thesis:

width N2 = 3 by MATRIX_0:23;
then ( 1 in Seg (width N2) & 2 in Seg (width N2) & 3 in Seg (width N2) ) by FINSEQ_1:1;
hence ( (Line (N2,1)) . 1 = N2 * (1,1) & (Line (N2,1)) . 2 = N2 * (1,2) & (Line (N2,1)) . 3 = N2 * (1,3) & (Line (N2,2)) . 1 = N2 * (2,1) & (Line (N2,2)) . 2 = N2 * (2,2) & (Line (N2,2)) . 3 = N2 * (2,3) & (Line (N2,3)) . 1 = N2 * (3,1) & (Line (N2,3)) . 2 = N2 * (3,2) & (Line (N2,3)) . 3 = N2 * (3,3) ) by MATRIX_0:def 7; :: thesis:
thus ( [1,1] in Indices N2 & [1,2] in Indices N2 & [1,3] in Indices N2 & [2,1] in Indices N2 & [2,2] in Indices N2 & [2,3] in Indices N2 & [3,1] in Indices N2 & [3,2] in Indices N2 & [3,3] in Indices N2 ) by ANPROJ_8:1, MATRIX_0:23; :: thesis:

end;

then reconsider l11 = (Line (N2,1)) . 1, l12 = (Line (N2,1)) . 2, l13 = (Line (N2,1)) . 3, l21 = (Line (N2,2)) . 1, l22 = (Line (N2,2)) . 2, l23 = (Line (N2,2)) . 3, l31 = (Line (N2,3)) . 1, l32 = (Line (N2,3)) . 2, l33 = (Line (N2,3)) . 3 as Element of F_Real ;
reconsider ru121 = u12f . 1, ru122 = u12f . 2, ru123 = u12f . 3 as Element of F_Real by XREAL_0:def 1;
( len (Line (N2,1)) = width N2 & len (Line (N2,2)) = width N2 & len (Line (N2,3)) = width N2 ) by MATRIX_0:def 7;
then A51: ( Line (N2,1) = <*l11,l12,l13*> & Line (N2,2) = <*l21,l22,l23*> & Line (N2,3) = <*l31,l32,l33*> ) by MATRIX_0:23, FINSEQ_1:45;
reconsider ru21 = u2 . 1, ru22 = u2 . 2, ru23 = u2 . 3 as Element of F_Real by XREAL_0:def 1;
A52: ( ru21 = a * (u12f . 1) & ru22 = a * (u12f . 2) & ru23 = a * (u12f . 3) ) by A3, A23, RVSUM_1:44;
len u2 = 3 by A29, EUCLID_8:50;
then A53: u2f = <*ru21,ru22,ru23*> by A10, FINSEQ_1:45;
reconsider t121 = v12 . 1, t122 = v12 . 2, t123 = v12 . 3 as Element of F_Real by A37;
reconsider v12f = v12 as FinSequence of F_Real by RVSUM_1:145;
width N1 = 3 by MATRIX_0:24;
then A54: width N1 = len N2 by MATRIX_0:24;
A55: ( [1,1] in Indices (N1 * N2) & [1,2] in Indices (N1 * N2) & [1,3] in Indices (N1 * N2) & [2,1] in Indices (N1 * N2) & [2,2] in Indices (N1 * N2) & [2,3] in Indices (N1 * N2) & [3,1] in Indices (N1 * N2) & [3,2] in Indices (N1 * N2) & [3,3] in Indices (N1 * N2) ) by ANPROJ_8:1, MATRIX_0:23;
A56: width (N1 * N2) = len (<*u12f*> @) by A34, MATRIX_0:24;
u12 in TOP-REAL 3 ;
then u12f in REAL 3 by EUCLID:22, A3;
then A57: len u12f = 3 by EUCLID_8:50;
(N1 * N2) * (<*u12f*> @) is Matrix of 3,1,F_Real by A3, FINSEQ_3:153, ANPROJ_8:91;
then A58: ( [1,1] in Indices ((N1 * N2) * (<*u12f*> @)) & [2,1] in Indices ((N1 * N2) * (<*u12f*> @)) & [3,1] in Indices ((N1 * N2) * (<*u12f*> @)) ) by MATRIX_0:23, ANPROJ_8:2;
A59: u12f = <*ru121,ru122,ru123*> by A57, FINSEQ_1:45;
A60: ( Col (N2,1) = <*l11,l21,l31*> & Col (N2,2) = <*l12,l22,l32*> & Col (N2,3) = <*l13,l23,l33*> )

proof

now :: thesis:

len N2 = 3 by MATRIX_0:24;
hence ( len (Col (N2,1)) = 3 & len (Col (N2,2)) = 3 & len (Col (N2,3)) = 3 ) by MATRIX_0:def 8; :: thesis:
( len N2 = 3 & width N2 = 3 ) by MATRIX_0:24;
then ( dom N2 = Seg 3 & Seg (width N2) = Seg 3 ) by FINSEQ_1:def 3;
then ( 1 in dom N2 & 2 in dom N2 & 3 in dom N2 & 1 in Seg (width N2) & 2 in Seg (width N2) & 3 in Seg (width N2) ) by FINSEQ_1:1;
hence ( (Col (N2,1)) . 1 = l11 & (Col (N2,2)) . 1 = l12 & (Col (N2,3)) . 1 = l13 & (Col (N2,1)) . 2 = l21 & (Col (N2,2)) . 2 = l22 & (Col (N2,3)) . 2 = l23 & (Col (N2,1)) . 3 = l31 & (Col (N2,2)) . 3 = l32 & (Col (N2,3)) . 3 = l33 ) by MATRIX_0:42; :: thesis:

end;

hence ( Col (N2,1) = <*l11,l21,l31*> & Col (N2,2) = <*l12,l22,l32*> & Col (N2,3) = <*l13,l23,l33*> ) by FINSEQ_1:45; :: thesis:

end;

Dir v1 = Dir v12

proof

ex c being Real st
( c <> 0 & v1 = c * v12 )

proof

set c = a * b;
take a * b ; :: thesis:
thus a * b <> 0 by A22, A24, XCMPLX_1:6; :: thesis:

A61: now :: thesis:

thus (N1 * (<*u1f*> @)) * (1,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1)) :: thesis:

proof

v1 . 1 = (a * b) * (v12 . 1)

proof

reconsider s1 = N1 * (1,1), s2 = N1 * (1,2), s3 = N1 * (1,3) as Element of F_Real ;
A62: (Line (N1,1)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7
.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;
reconsider s121 = (N1 * N2) * (1,1), s122 = (N1 * N2) * (1,2), s123 = (N1 * N2) * (1,3) as Element of F_Real ;
A63: t121 = ((N1 * N2) * (<*u12f*> @)) * (1,1) by A37
.= (Line ((N1 * N2),1)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4
.= (Line ((N1 * N2),1)) "*" u12f by ANPROJ_8:93
.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45
.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

now :: thesis:

thus s121 = (Line (N1,1)) "*" (Col (N2,1)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis:
thus s122 = (Line (N1,1)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis:
thus s123 = (Line (N1,1)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis:

end;

then (a * b) * t121 = b * ((Line (N1,1)) "*" v2f) by A63, A62
.= (N1 * (<*u1f*> @)) * (1,1) by A39, XCMPLX_1:52
.= v1 . 1 by A28 ;
hence v1 . 1 = (a * b) * (v12 . 1) ; :: thesis:

end;

hence (N1 * (<*u1f*> @)) * (1,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1)) by A45, A37; :: thesis:

end;

thus (N1 * (<*u1f*> @)) * (2,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1)) :: thesis:

proof

v1 . 2 = (a * b) * (v12 . 2)

proof

reconsider s1 = N1 * (2,1), s2 = N1 * (2,2), s3 = N1 * (2,3) as Element of F_Real ;
A64: (Line (N1,2)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7
.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;
reconsider s121 = (N1 * N2) * (2,1), s122 = (N1 * N2) * (2,2), s123 = (N1 * N2) * (2,3) as Element of F_Real ;
A65: t122 = ((N1 * N2) * (<*u12f*> @)) * (2,1) by A37
.= (Line ((N1 * N2),2)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4
.= (Line ((N1 * N2),2)) "*" u12f by ANPROJ_8:93
.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45
.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

now :: thesis:

thus s121 = (Line (N1,2)) "*" (Col (N2,1)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis:
thus s122 = (Line (N1,2)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis:
thus s123 = (Line (N1,2)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis:

end;

then (a * b) * t122 = b * ((Line (N1,2)) "*" v2f) by A65, A64
.= (N1 * (<*u1f*> @)) * (2,1) by A39, XCMPLX_1:52
.= v1 . 2 by A28 ;
hence v1 . 2 = (a * b) * (v12 . 2) ; :: thesis:

end;

hence (N1 * (<*u1f*> @)) * (2,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1)) by A45, A37; :: thesis:

end;

thus (N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1)) :: thesis:

proof

v1 . 3 = (a * b) * (v12 . 3)

proof

reconsider s1 = N1 * (3,1), s2 = N1 * (3,2), s3 = N1 * (3,3) as Element of F_Real ;
A66: (Line (N1,3)) "*" v2f = ((s1 * (<*l11,l12,l13*> "*" <*ru21,ru22,ru23*>)) + (s2 * (<*l21,l22,l23*> "*" <*ru21,ru22,ru23*>))) + (s3 * (<*l31,l32,l33*> "*" <*ru21,ru22,ru23*>)) by A51, A53, A48, A49, A50, A42, A46, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * ((Line (N2,2)) "*" u2f))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * ((Line (N2,3)) "*" u2f)) by A51, A53, ANPROJ_8:7
.= ((s1 * (((l11 * ru21) + (l12 * ru22)) + (l13 * ru23))) + (s2 * (((l21 * ru21) + (l22 * ru22)) + (l23 * ru23)))) + (s3 * (((l31 * ru21) + (l32 * ru22)) + (l33 * ru23))) by A51, A53, ANPROJ_8:7
.= a * ((((((s1 * l11) + (s2 * l21)) + (s3 * l31)) * ru121) + ((((s1 * l12) + (s2 * l22)) + (s3 * l32)) * ru122)) + ((((s1 * l13) + (s2 * l23)) + (s3 * l33)) * ru123)) by A52 ;
reconsider s121 = (N1 * N2) * (3,1), s122 = (N1 * N2) * (3,2), s123 = (N1 * N2) * (3,3) as Element of F_Real ;
A67: t123 = ((N1 * N2) * (<*u12f*> @)) * (3,1) by A37
.= (Line ((N1 * N2),3)) "*" (Col ((<*u12f*> @),1)) by A56, A58, MATRIX_3:def 4
.= (Line ((N1 * N2),3)) "*" u12f by ANPROJ_8:93
.= <*s121,s122,s123*> "*" <*ru121,ru122,ru123*> by A59, A44, A43, MATRIX_0:24, FINSEQ_1:45
.= ((s121 * ru121) + (s122 * ru122)) + (s123 * ru123) by ANPROJ_8:7 ;

now :: thesis:

thus s121 = (Line (N1,3)) "*" (Col (N2,1)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,1)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l11) + (s2 * l21)) + (s3 * l31) by A60, ANPROJ_8:7 ; :: thesis:
thus s122 = (Line (N1,3)) "*" (Col (N2,2)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,2)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l12) + (s2 * l22)) + (s3 * l32) by A60, ANPROJ_8:7 ; :: thesis:
thus s123 = (Line (N1,3)) "*" (Col (N2,3)) by A54, A55, MATRIX_3:def 4
.= <*s1,s2,s3*> "*" (Col (N2,3)) by A41, A40, MATRIX_0:24, FINSEQ_1:45
.= ((s1 * l13) + (s2 * l23)) + (s3 * l33) by A60, ANPROJ_8:7 ; :: thesis:

end;

then (a * b) * t123 = b * ((Line (N1,3)) "*" v2f) by A67, A66
.= (N1 * (<*u1f*> @)) * (3,1) by A39, XCMPLX_1:52
.= v1 . 3 by A28 ;
hence v1 . 3 = (a * b) * (v12 . 3) ; :: thesis:

end;

hence (N1 * (<*u1f*> @)) * (3,1) = (a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1)) by A45, A37; :: thesis:

end;

<*((a * b) * (((N1 * N2) * (<*u12f*> @)) * (1,1))),((a * b) * (((N1 * N2) * (<*u12f*> @)) * (2,1))),((a * b) * (((N1 * N2) * (<*u12f*> @)) * (3,1)))*> = (a * b) * |[(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))]| by EUCLID_5:8
.= (a * b) * <*(((N1 * N2) * (<*u12f*> @)) * (1,1)),(((N1 * N2) * (<*u12f*> @)) * (2,1)),(((N1 * N2) * (<*u12f*> @)) * (3,1))*> ;
hence v1 = (a * b) * v12 by A28, A37, A61; :: thesis:

end;

then are_Prop v1,v12 by ANPROJ_1:1;
hence Dir v1 = Dir v12 by A6, A20, ANPROJ_1:22; :: thesis:

end;

hence (homography N1) . ((homography N2) . P) = (homography (N1 * N2)) . P by A7, A21; :: thesis: