anproj_9.miz



    begin

    reserve i,n for Nat;

    reserve r for Real;

    reserve ra for Element of F_Real ;

    reserve a,b,c for non zero Element of F_Real ;

    reserve u,v for Element of ( TOP-REAL 3);

    reserve p1 for FinSequence of (1 -tuples_on REAL );

    reserve pf,uf for FinSequence of F_Real ;

    reserve N for Matrix of 3, F_Real ;

    reserve K for Field;

    reserve k for Element of K;

    theorem :: ANPROJ_9:1

    

     Th01: ( 1. ( F_Real ,3)) = <* <*1, 0 , 0 *>, <* 0 , 1, 0 *>, <* 0 , 0 , 1*>*>

    proof

      

       A1: ( len ( 1. ( F_Real ,3))) = 3 by MATRIX_0: 23;

      1 in ( Seg 3) & 2 in ( Seg 3) & 3 in ( Seg 3) by FINSEQ_1: 1;

      then (( 1. ( F_Real ,3)) . 1) = ( Line (( 1. ( F_Real ,3)),1)) & (( 1. ( F_Real ,3)) . 2) = ( Line (( 1. ( F_Real ,3)),2)) & (( 1. ( F_Real ,3)) . 3) = ( Line (( 1. ( F_Real ,3)),3)) by MATRIX_0: 52;

      hence thesis by A1, FINSEQ_1: 45, ANPROJ_8: 68;

    end;

    theorem :: ANPROJ_9:2

    

     Th02: (ra * N) = ((ra * ( 1. ( F_Real ,3))) * N)

    proof

      ( width ( 1. ( F_Real ,3))) = 3 by MATRIX_0: 24;

      then

       A1: ( width ( 1. ( F_Real ,3))) = ( len N) by MATRIX_0: 24;

      (ra * N) = (ra * (( 1. ( F_Real ,3)) * N)) by MATRIX_3: 18;

      hence thesis by A1, MATRIX15: 1;

    end;

    theorem :: ANPROJ_9:3

    

     Th04: r <> 0 & u is non zero implies (r * u) is non zero

    proof

      assume that

       A1: r <> 0 and

       A2: u is non zero;

      (r * u) <> ( 0. ( TOP-REAL 3))

      proof

        assume

         A3: (r * u) = ( 0. ( TOP-REAL 3));

        u = (1 * u) by RVSUM_1: 52

        .= (((1 / r) * r) * u) by A1, XCMPLX_1: 87

        .= ((1 / r) * ( 0. ( TOP-REAL 3))) by A3, RVSUM_1: 49

        .= ( 0. ( TOP-REAL 3));

        hence contradiction by A2;

      end;

      hence thesis;

    end;

    theorem :: ANPROJ_9:4

    

     Th05: for a11,a12,a13,a21,a22,a23,a31,a32,a33 be Element of F_Real holds for A be Matrix of 3, F_Real st A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> holds ( Line (A,1)) = <*a11, a12, a13*> & ( Line (A,2)) = <*a21, a22, a23*> & ( Line (A,3)) = <*a31, a32, a33*>

    proof

      let a11,a12,a13,a21,a22,a23,a31,a32,a33 be Element of F_Real ;

      let A be Matrix of 3, F_Real ;

      assume A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*>;

      then

       A1: (A . 1) = <*a11, a12, a13*> & (A . 2) = <*a21, a22, a23*> & (A . 3) = <*a31, a32, a33*> by FINSEQ_1: 45;

      1 in ( Seg 3) & 2 in ( Seg 3) & 3 in ( Seg 3) by FINSEQ_1: 1;

      hence thesis by A1, MATRIX_0: 52;

    end;

    theorem :: ANPROJ_9:5

    

     Th06: for a11,a12,a13,a21,a22,a23,a31,a32,a33 be Element of F_Real holds for A be Matrix of 3, F_Real st A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> holds ( Col (A,1)) = <*a11, a21, a31*> & ( Col (A,2)) = <*a12, a22, a32*> & ( Col (A,3)) = <*a13, a23, a33*>

    proof

      let a11,a12,a13,a21,a22,a23,a31,a32,a33 be Element of F_Real ;

      let A be Matrix of 3, F_Real ;

      assume

       A1: A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*>;

       |[a11, a12, a13]| is Point of ( TOP-REAL 3) & |[a21, a22, a23]| is Point of ( TOP-REAL 3) & |[a31, a32, a33]| is Point of ( TOP-REAL 3);

      then

      reconsider p = <*a11, a12, a13*>, q = <*a21, a22, a23*>, r = <*a31, a32, a33*> as Point of ( TOP-REAL 3);

      (p . 1) = a11 & (p . 2) = a12 & (p . 3) = a13 & (q . 1) = a21 & (q . 2) = a22 & (q . 3) = a23 & (r . 1) = a31 & (r . 2) = a32 & (r . 3) = a33 by FINSEQ_1: 45;

      then

       A2: (p `1 ) = a11 & (p `2 ) = a12 & (p `3 ) = a13 & (q `1 ) = a21 & (q `2 ) = a22 & (q `3 ) = a23 & (r `1 ) = a31 & (r `2 ) = a32 & (r `3 ) = a33 by EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

      (A @ ) = <* <*(p `1 ), (q `1 ), (r `1 )*>, <*(p `2 ), (q `2 ), (r `2 )*>, <*(p `3 ), (q `3 ), (r `3 )*>*> by A1, ANPROJ_8: 23;

      then

       A3: ( Line ((A @ ),1)) = <*a11, a21, a31*> & ( Line ((A @ ),2)) = <*a12, a22, a32*> & ( Line ((A @ ),3)) = <*a13, a23, a33*> by A2, Th05;

      

       A4: ( width A) = 3 by MATRIX_0: 24;

      1 in ( Seg 3) & 2 in ( Seg 3) & 3 in ( Seg 3) by FINSEQ_1: 1;

      hence thesis by A3, A4, MATRIX_0: 59;

    end;

    theorem :: ANPROJ_9:6

    

     Th07: for a11,a12,a13,a21,a22,a23,a31,a32,a33,b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real holds for A,B be Matrix of 3, F_Real st A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> & B = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*> holds (A * B) = <* <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)), (((a11 * b12) + (a12 * b22)) + (a13 * b32)), (((a11 * b13) + (a12 * b23)) + (a13 * b33))*>, <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)), (((a21 * b12) + (a22 * b22)) + (a23 * b32)), (((a21 * b13) + (a22 * b23)) + (a23 * b33))*>, <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)), (((a31 * b12) + (a32 * b22)) + (a33 * b32)), (((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*>

    proof

      let a11,a12,a13,a21,a22,a23,a31,a32,a33,b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real ;

      let A,B be Matrix of 3, F_Real ;

      assume that

       A1: A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> and

       A2: B = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*>;

      

       A3: ( width A) = 3 & ( len B) = 3 by MATRIX_0: 23;

      

       A4: [1, 1] in ( Indices (A * B)) & [1, 2] in ( Indices (A * B)) & [1, 3] in ( Indices (A * B)) & [2, 1] in ( Indices (A * B)) & [2, 2] in ( Indices (A * B)) & [2, 3] in ( Indices (A * B)) & [3, 1] in ( Indices (A * B)) & [3, 2] in ( Indices (A * B)) & [3, 3] in ( Indices (A * B)) by ANPROJ_8: 1, MATRIX_0: 23;

      

       A5: ( Line (A,1)) = <*a11, a12, a13*> & ( Line (A,2)) = <*a21, a22, a23*> & ( Line (A,3)) = <*a31, a32, a33*> by A1, Th05;

      

       A6: ( Col (B,1)) = <*b11, b21, b31*> & ( Col (B,2)) = <*b12, b22, b32*> & ( Col (B,3)) = <*b13, b23, b33*> by A2, Th06;

      now

        

        thus ((A * B) * (1,1)) = (( Line (A,1)) "*" ( Col (B,1))) by A3, A4, MATRIX_3:def 4

        .= (((a11 * b11) + (a12 * b21)) + (a13 * b31)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (1,2)) = (( Line (A,1)) "*" ( Col (B,2))) by A3, A4, MATRIX_3:def 4

        .= (((a11 * b12) + (a12 * b22)) + (a13 * b32)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (1,3)) = (( Line (A,1)) "*" ( Col (B,3))) by A3, A4, MATRIX_3:def 4

        .= (((a11 * b13) + (a12 * b23)) + (a13 * b33)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (2,1)) = (( Line (A,2)) "*" ( Col (B,1))) by A3, A4, MATRIX_3:def 4

        .= (((a21 * b11) + (a22 * b21)) + (a23 * b31)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (2,2)) = (( Line (A,2)) "*" ( Col (B,2))) by A3, A4, MATRIX_3:def 4

        .= (((a21 * b12) + (a22 * b22)) + (a23 * b32)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (2,3)) = (( Line (A,2)) "*" ( Col (B,3))) by A3, A4, MATRIX_3:def 4

        .= (((a21 * b13) + (a22 * b23)) + (a23 * b33)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (3,1)) = (( Line (A,3)) "*" ( Col (B,1))) by A3, A4, MATRIX_3:def 4

        .= (((a31 * b11) + (a32 * b21)) + (a33 * b31)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (3,2)) = (( Line (A,3)) "*" ( Col (B,2))) by A3, A4, MATRIX_3:def 4

        .= (((a31 * b12) + (a32 * b22)) + (a33 * b32)) by A5, A6, ANPROJ_8: 7;

        

        thus ((A * B) * (3,3)) = (( Line (A,3)) "*" ( Col (B,3))) by A3, A4, MATRIX_3:def 4

        .= (((a31 * b13) + (a32 * b23)) + (a33 * b33)) by A5, A6, ANPROJ_8: 7;

      end;

      hence thesis by MATRIXR2: 37;

    end;

    theorem :: ANPROJ_9:7

    

     Th08: for a11,a12,a13,a21,a22,a23,a31,a32,a33,b1,b2,b3 be Element of F_Real holds for A be Matrix of 3, 3, F_Real holds for B be Matrix of 3, 1, F_Real st A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> & B = <* <*b1*>, <*b2*>, <*b3*>*> holds (A * B) = <* <*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*>, <*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*>, <*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*>*>

    proof

      let a11,a12,a13,a21,a22,a23,a31,a32,a33,b1,b2,b3 be Element of F_Real ;

      let A be Matrix of 3, 3, F_Real ;

      let B be Matrix of 3, 1, F_Real ;

      assume that

       A1: A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> and

       A2: B = <* <*b1*>, <*b2*>, <*b3*>*>;

      

       A3: ( width A) = 3 & ( len B) = 3 & ( len A) = 3 & ( width B) = 1 by MATRIX_0: 23;

      

       A4: ( len (A * B)) = 3 & ( width (A * B)) = 1 by A3, MATRIX_3:def 4;

      

       A5: (A * B) is Matrix of 3, 1, F_Real by A4, MATRIX_0: 20;

      then

       A6: [1, 1] in ( Indices (A * B)) & [2, 1] in ( Indices (A * B)) & [3, 1] in ( Indices (A * B)) by ANPROJ_8: 2, MATRIX_0: 23;

      

       A7: ( Line (A,1)) = <*a11, a12, a13*> & ( Line (A,2)) = <*a21, a22, a23*> & ( Line (A,3)) = <*a31, a32, a33*> by A1, Th05;

      1 in ( Seg 3) & 2 in ( Seg 3) & 3 in ( Seg 3) by FINSEQ_1: 1;

      then

       A8: 1 in ( dom B) & 2 in ( dom B) & 3 in ( dom B) by FINSEQ_1:def 3, A3;

      now

        thus ( len ( Col (B,1))) = 3 by A3, MATRIX_0:def 8;

         [1, 1] in ( Indices B) by MATRIX_0: 23, ANPROJ_8: 2;

        then

        consider p be FinSequence of F_Real such that

         A9: p = (B . 1) and

         A10: (B * (1,1)) = (p . 1) by MATRIX_0:def 5;

        (B * (1,1)) = ( <*b1*> . 1) by A9, A10, A2, FINSEQ_1: 45

        .= b1 by FINSEQ_1:def 8;

        hence (( Col (B,1)) . 1) = b1 by A8, MATRIX_0:def 8;

         [2, 1] in ( Indices B) by MATRIX_0: 23, ANPROJ_8: 2;

        then

        consider p be FinSequence of F_Real such that

         A11: p = (B . 2) and

         A12: (B * (2,1)) = (p . 1) by MATRIX_0:def 5;

        (B * (2,1)) = ( <*b2*> . 1) by A11, A12, A2, FINSEQ_1: 45

        .= b2 by FINSEQ_1:def 8;

        hence (( Col (B,1)) . 2) = b2 by A8, MATRIX_0:def 8;

         [3, 1] in ( Indices B) by MATRIX_0: 23, ANPROJ_8: 2;

        then

        consider p be FinSequence of F_Real such that

         A13: p = (B . 3) and

         A14: (B * (3,1)) = (p . 1) by MATRIX_0:def 5;

        (B * (3,1)) = ( <*b3*> . 1) by A13, A14, A2, FINSEQ_1: 45

        .= b3 by FINSEQ_1:def 8;

        hence (( Col (B,1)) . 3) = b3 by A8, MATRIX_0:def 8;

      end;

      then

       A15: ( Col (B,1)) = <*b1, b2, b3*> by FINSEQ_1: 45;

      now

        

        thus ((A * B) * (1,1)) = (( Line (A,1)) "*" ( Col (B,1))) by A3, A6, MATRIX_3:def 4

        .= (((a11 * b1) + (a12 * b2)) + (a13 * b3)) by A7, A15, ANPROJ_8: 7;

        

        thus ((A * B) * (2,1)) = (( Line (A,2)) "*" ( Col (B,1))) by A3, A6, MATRIX_3:def 4

        .= (((a21 * b1) + (a22 * b2)) + (a23 * b3)) by A7, A15, ANPROJ_8: 7;

        

        thus ((A * B) * (3,1)) = (( Line (A,3)) "*" ( Col (B,1))) by A3, A6, MATRIX_3:def 4

        .= (((a31 * b1) + (a32 * b2)) + (a33 * b3)) by A7, A15, ANPROJ_8: 7;

      end;

      then

       A16: ( Line ((A * B),1)) = <*(((a11 * b1) + (a12 * b2)) + (a13 * b3))*> & ( Line ((A * B),2)) = <*(((a21 * b1) + (a22 * b2)) + (a23 * b3))*> & ( Line ((A * B),3)) = <*(((a31 * b1) + (a32 * b2)) + (a33 * b3))*> by A5, ANPROJ_8: 90;

      now

        thus ( len (A * B)) = 3 by A3, MATRIX_3:def 4;

        1 in ( Seg 3) & 2 in ( Seg 3) & 3 in ( Seg 3) by FINSEQ_1: 1;

        hence ((A * B) . 1) = ( Line ((A * B),1)) & ((A * B) . 2) = ( Line ((A * B),2)) & ((A * B) . 3) = ( Line ((A * B),3)) by A5, MATRIX_0: 52;

      end;

      hence thesis by A16, FINSEQ_1: 45;

    end;

    

     Lem01: for a11,a12,a13,a21,a22,a23,a31,a32,a33,b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real holds for A,B be Matrix of 3, F_Real st A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> & B = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*> holds ((A * B) . 1) = <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)), (((a11 * b12) + (a12 * b22)) + (a13 * b32)), (((a11 * b13) + (a12 * b23)) + (a13 * b33))*> & ((A * B) . 2) = <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)), (((a21 * b12) + (a22 * b22)) + (a23 * b32)), (((a21 * b13) + (a22 * b23)) + (a23 * b33))*> & ((A * B) . 3) = <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)), (((a31 * b12) + (a32 * b22)) + (a33 * b32)), (((a31 * b13) + (a32 * b23)) + (a33 * b33))*>

    proof

      let a11,a12,a13,a21,a22,a23,a31,a32,a33,b11,b12,b13,b21,b22,b23,b31,b32,b33 be Element of F_Real ;

      let A,B be Matrix of 3, F_Real ;

      assume that

       A1: A = <* <*a11, a12, a13*>, <*a21, a22, a23*>, <*a31, a32, a33*>*> and

       A2: B = <* <*b11, b12, b13*>, <*b21, b22, b23*>, <*b31, b32, b33*>*>;

      now

        now

          thus ( len A) = 3 by A1, FINSEQ_1: 45;

          ( width A) = 3 & ( len B) = 3 by MATRIX_0: 23;

          hence ( len (A * B)) = ( len A) by MATRIX_3:def 4;

        end;

        hence ( len (A * B)) = 3;

        thus (A * B) = <* <*(((a11 * b11) + (a12 * b21)) + (a13 * b31)), (((a11 * b12) + (a12 * b22)) + (a13 * b32)), (((a11 * b13) + (a12 * b23)) + (a13 * b33))*>, <*(((a21 * b11) + (a22 * b21)) + (a23 * b31)), (((a21 * b12) + (a22 * b22)) + (a23 * b32)), (((a21 * b13) + (a22 * b23)) + (a23 * b33))*>, <*(((a31 * b11) + (a32 * b21)) + (a33 * b31)), (((a31 * b12) + (a32 * b22)) + (a33 * b32)), (((a31 * b13) + (a32 * b23)) + (a33 * b33))*>*> by A1, A2, Th07;

      end;

      hence thesis by FINSEQ_1: 45;

    end;

    theorem :: ANPROJ_9:8

    

     Th09: for a,b,c be non zero Element of F_Real holds for M1,M2 be Matrix of 3, F_Real st M1 = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> & M2 = <* <*(1 / a), 0 , 0 *>, <* 0 , (1 / b), 0 *>, <* 0 , 0 , (1 / c)*>*> holds (M1 * M2) = ( 1. ( F_Real ,3)) & (M2 * M1) = ( 1. ( F_Real ,3))

    proof

      let a,b,c be non zero Element of F_Real ;

      let M1,M2 be Matrix of 3, F_Real ;

      assume that

       A1: M1 = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> and

       A2: M2 = <* <*(1 / a), 0 , 0 *>, <* 0 , (1 / b), 0 *>, <* 0 , 0 , (1 / c)*>*>;

      reconsider z = 0 as Element of F_Real ;

      reconsider ia = (1 / a), ib = (1 / b), ic = (1 / c) as Element of F_Real by XREAL_0:def 1;

      

       A4: M2 = <* <*ia, z, z*>, <*z, ib, z*>, <*z, z, ic*>*> by A2;

      a is non zero;

      then

       A5: (a * ia) = 1 & (b * ib) = 1 & (c * ic) = 1 by XCMPLX_1: 106;

      

       A6: ( len (M1 * M2)) = 3 by MATRIX_0: 23;

      ((M1 * M2) . 1) = <*(((a * ia) + (z * z)) + (z * z)), (((a * z) + (z * ib)) + (z * z)), (((a * z) + (z * z)) + (z * ic))*> & ((M1 * M2) . 2) = <*(((z * ia) + (b * z)) + (z * z)), (((z * z) + (b * ib)) + (z * z)), (((z * z) + (b * z)) + (z * ic))*> & ((M1 * M2) . 3) = <*(((z * ia) + (z * z)) + (c * z)), (((z * z) + (z * ib)) + (c * z)), (((z * z) + (z * z)) + (c * ic))*> by A1, A2, Lem01;

      hence (M1 * M2) = ( 1. ( F_Real ,3)) by A6, A5, FINSEQ_1: 45, Th01;

      

       A7: ( len (M2 * M1)) = 3 by MATRIX_0: 23;

      ((M2 * M1) . 1) = <*(((ia * a) + (z * z)) + (z * z)), (((ia * z) + (z * b)) + (z * z)), (((ia * z) + (z * z)) + (z * c))*> & ((M2 * M1) . 2) = <*(((z * a) + (ib * z)) + (z * z)), (((z * z) + (ib * b)) + (z * z)), (((z * z) + (ib * z)) + (z * c))*> & ((M2 * M1) . 3) = <*(((z * a) + (z * z)) + (ic * z)), (((z * z) + (z * b)) + (ic * z)), (((z * z) + (z * z)) + (ic * c))*> by A1, A4, Lem01;

      hence (M2 * M1) = ( 1. ( F_Real ,3)) by A7, A5, FINSEQ_1: 45, Th01;

    end;

    theorem :: ANPROJ_9:9

    

     Th10: for a,b,c be non zero Element of F_Real holds <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> is invertible Matrix of 3, F_Real

    proof

      let a,b,c be non zero Element of F_Real ;

      reconsider ia = (1 / a), ib = (1 / b), ic = (1 / c) as Element of F_Real by XREAL_0:def 1;

      reconsider M = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*>, N = <* <*ia, 0 , 0 *>, <* 0 , ib, 0 *>, <* 0 , 0 , ic*>*> as Matrix of 3, F_Real by MATRIXR2: 35;

      now

        thus (N * M) = ( 1. ( F_Real ,3)) by Th09;

        hence (N * M) = (M * N) by Th09;

      end;

      hence thesis by MATRIX_6:def 2, MATRIX_6:def 3;

    end;

    theorem :: ANPROJ_9:10

    

     Th11: |[1, 0 , 0 ]| is non zero & |[ 0 , 1, 0 ]| is non zero & |[ 0 , 0 , 1]| is non zero & |[1, 1, 1]| is non zero by EUCLID_5: 4, FINSEQ_1: 78;

    theorem :: ANPROJ_9:11

     |[1, 0 , 0 ]| <> ( 0. ( TOP-REAL 3)) & |[ 0 , 1, 0 ]| <> ( 0. ( TOP-REAL 3)) & |[ 0 , 0 , 1]| <> ( 0. ( TOP-REAL 3)) & |[1, 1, 1]| <> ( 0. ( TOP-REAL 3))

    proof

       |[1, 0 , 0 ]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[1, 0 , 0 ]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `1 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence |[1, 0 , 0 ]| <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4;

       |[ 0 , 1, 0 ]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[ 0 , 1, 0 ]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `2 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence |[ 0 , 1, 0 ]| <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4;

       |[ 0 , 0 , 1]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[ 0 , 0 , 1]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `3 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence |[ 0 , 0 , 1]| <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4;

       |[1, 1, 1]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[1, 1, 1]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `1 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence |[1, 1, 1]| <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4;

    end;

    theorem :: ANPROJ_9:12

    

     Th13: <e1> <> ( 0. ( TOP-REAL 3)) & <e2> <> ( 0. ( TOP-REAL 3)) & <e3> <> ( 0. ( TOP-REAL 3))

    proof

       |[1, 0 , 0 ]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[1, 0 , 0 ]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `1 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence <e1> <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4, EUCLID_8:def 1;

       |[ 0 , 1, 0 ]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[ 0 , 1, 0 ]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `2 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence <e2> <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4, EUCLID_8:def 2;

       |[ 0 , 0 , 1]| <> |[ 0 , 0 , 0 ]|

      proof

        assume |[ 0 , 0 , 1]| = |[ 0 , 0 , 0 ]|;

        then 1 = ( |[ 0 , 0 , 0 ]| `3 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

      hence <e3> <> ( 0. ( TOP-REAL 3)) by EUCLID_5: 4, EUCLID_8:def 3;

    end;

    begin

    

     Lem02: i in ( Seg 3) & u = uf & p1 = (N * uf) implies (p1 . i) = <*((N * ( <*uf*> @ )) * (i,1))*>

    proof

      assume that

       A1: i in ( Seg 3) and

       A2: u = uf and

       A3: p1 = (N * uf);

      

       A4: (N * ( <*uf*> @ )) is Matrix of 3, 1, F_Real by A2, FINSEQ_3: 153, ANPROJ_8: 91;

      u in ( TOP-REAL 3);

      then u in ( REAL 3) by EUCLID: 22;

      then

       A5: 3 = ( len uf) by A2, EUCLID_8: 50;

      

       A6: i = 1 or ... or i = 3 by A1, FINSEQ_1: 91;

      p1 = (N * ( <*uf*> @ )) by A3, LAPLACE:def 9;

      

      then (p1 . i) = ( Line ((N * ( <*uf*> @ )),i)) by A1, A4, MATRIX_0: 52

      .= <*((N * ( <*uf*> @ )) * (i,1))*> by A6, A5, ANPROJ_8: 92;

      hence thesis;

    end;

    

     Lem03: i in ( Seg 3) & u = uf & pf = v & r <> 0 & v = (r * u) implies ((N * ( <*uf*> @ )) * (i,1)) = ((1 / r) * (( Line (N,i)) "*" pf))

    proof

      assume that

       A1: i in ( Seg 3) and

       A2: u = uf and

       A3: pf = v and

       A4: r <> 0 and

       A5: v = (r * u);

      set b = (1 / r);

      reconsider s1 = (uf . 1), s2 = (uf . 2), s3 = (uf . 3) as Element of F_Real by XREAL_0:def 1;

      u in ( TOP-REAL 3);

      then

       A6: u in ( REAL 3) by EUCLID: 22;

      

       A7: ( width <*uf*>) = ( len u) by A2, ANPROJ_8: 75

      .= 3 by A6, EUCLID_8: 50;

      

       A8: ( width N) = 3 by MATRIX_0: 24

      .= ( len ( <*uf*> @ )) by MATRIX_0:def 6, A7;

      (N * ( <*uf*> @ )) is Matrix of 3, 1, F_Real by A2, FINSEQ_3: 153, ANPROJ_8: 91;

      then

       A9: [1, 1] in ( Indices (N * ( <*uf*> @ ))) & [2, 1] in ( Indices (N * ( <*uf*> @ ))) & [3, 1] in ( Indices (N * ( <*uf*> @ ))) by MATRIX_0: 23, ANPROJ_8: 2;

      reconsider t1 = (v . 1), t2 = (v . 2), t3 = (v . 3) as Element of F_Real by XREAL_0:def 1;

      

       A10: ( len N) = 3 & ( width N) = 3 by MATRIX_0: 23;

       A11:

      now

        

        thus ( len ( Line (N,1))) = ( width N) by MATRIX_0:def 7

        .= 3 by MATRIX_0: 23;

        1 in ( Seg ( width N)) & 2 in ( Seg ( width N)) & 3 in ( Seg ( width N)) by A10, FINSEQ_1: 1;

        hence (( Line (N,1)) . 1) = (N * (1,1)) & (( Line (N,1)) . 2) = (N * (1,2)) & (( Line (N,1)) . 3) = (N * (1,3)) by MATRIX_0:def 7;

      end;

       A12:

      now

        

        thus ( len ( Line (N,2))) = ( width N) by MATRIX_0:def 7

        .= 3 by MATRIX_0: 23;

        1 in ( Seg ( width N)) & 2 in ( Seg ( width N)) & 3 in ( Seg ( width N)) by A10, FINSEQ_1: 1;

        hence (( Line (N,2)) . 1) = (N * (2,1)) & (( Line (N,2)) . 2) = (N * (2,2)) & (( Line (N,2)) . 3) = (N * (2,3)) by MATRIX_0:def 7;

      end;

       A13:

      now

        

        thus ( len ( Line (N,3))) = ( width N) by MATRIX_0:def 7

        .= 3 by MATRIX_0: 23;

        1 in ( Seg ( width N)) & 2 in ( Seg ( width N)) & 3 in ( Seg ( width N)) by A10, FINSEQ_1: 1;

        hence (( Line (N,3)) . 1) = (N * (3,1)) & (( Line (N,3)) . 2) = (N * (3,2)) & (( Line (N,3)) . 3) = (N * (3,3)) by MATRIX_0:def 7;

      end;

      3 = ( len uf) by A2, A6, EUCLID_8: 50;

      then

       A14: uf = <*s1, s2, s3*> by FINSEQ_1: 45;

      

       A15: i = 1 or ... or i = 3 by A1, FINSEQ_1: 91;

      

       A16: (b * v) = (((1 / r) * r) * uf) by A5, A2, RVSUM_1: 49

      .= (1 * uf) by A4, XCMPLX_1: 87

      .= uf by RVSUM_1: 52;

      uf in ( TOP-REAL 3) by A2;

      then

       A17: uf in ( REAL 3) by EUCLID: 22;

      v in ( TOP-REAL 3);

      then

       A18: v in ( REAL 3) by EUCLID: 22;

      

      then |[(b * (v . 1)), (b * (v . 2)), (b * (v . 3))]| = uf by A16, EUCLID_8: 52

      .= |[(uf . 1), (uf . 2), (uf . 3)]| by A17, EUCLID_8: 1;

      then

       A19: (b * (v . 1)) = (uf . 1) & (b * (v . 2)) = (uf . 2) & (b * (v . 3)) = (uf . 3) by FINSEQ_1: 78;

      

       A20: pf = <*t1, t2, t3*> by A3, A18, EUCLID_8: 1;

      ((N * ( <*uf*> @ )) * (i,1)) = (( Line (N,i)) "*" ( Col (( <*uf*> @ ),1))) by A15, A8, A9, MATRIX_3:def 4

      .= (( Line (N,i)) "*" uf) by ANPROJ_8: 93

      .= ( <*(N * (i,1)), (N * (i,2)), (N * (i,3))*> "*" <*s1, s2, s3*>) by A15, A11, A12, A13, FINSEQ_1: 45, A14

      .= ((((N * (i,1)) * s1) + ((N * (i,2)) * s2)) + ((N * (i,3)) * s3)) by ANPROJ_8: 7

      .= (b * ((((N * (i,1)) * t1) + ((N * (i,2)) * t2)) + ((N * (i,3)) * t3))) by A19

      .= (b * ( <*(N * (i,1)), (N * (i,2)), (N * (i,3))*> "*" <*t1, t2, t3*>)) by ANPROJ_8: 7

      .= (b * (( Line (N,i)) "*" pf)) by A15, A11, A12, A13, FINSEQ_1: 45, A20;

      hence thesis;

    end;

    

     Lem04: i in ( Seg 3) & u = uf & pf = v & p1 = (N * uf) & r <> 0 & v = (r * u) implies ((p1 . i) . 1) = ((1 / r) * (( Line (N,i)) "*" pf))

    proof

      assume that

       A1: i in ( Seg 3) and

       A2: u = uf and

       A3: pf = v and

       A4: p1 = (N * uf) and

       A5: r <> 0 and

       A6: v = (r * u);

      set b = (1 / r);

      

       A7: (p1 . 1) = <*((N * ( <*uf*> @ )) * (1,1))*> & (p1 . 2) = <*((N * ( <*uf*> @ )) * (2,1))*> & (p1 . 3) = <*((N * ( <*uf*> @ )) * (3,1))*> by A2, A4, FINSEQ_1: 1, Lem02;

      i = 1 or ... or i = 3 by A1, FINSEQ_1: 91;

      

      then ((p1 . i) . 1) = ((N * ( <*uf*> @ )) * (i,1)) by A7, FINSEQ_1: 40

      .= (b * (( Line (N,i)) "*" pf)) by A1, A2, A3, A5, A6, Lem03;

      hence thesis;

    end;

    

     Lem05: i in ( Seg 3) & pf = v implies (( Line (N,i)) "*" pf) = (((N * pf) . i) . 1)

    proof

      assume that

       A1: i in ( Seg 3) and

       A2: pf = v;

      

       A3: (N * ( <*pf*> @ )) is Matrix of 3, 1, F_Real by A2, FINSEQ_3: 153, ANPROJ_8: 91;

      v in ( TOP-REAL 3);

      then v in ( REAL 3) by EUCLID: 22;

      then

       A4: 3 = ( len pf) by A2, EUCLID_8: 50;

      v in ( TOP-REAL 3);

      then

       A5: v in ( REAL 3) by EUCLID: 22;

      

       A6: ( width <*pf*>) = ( len pf) by ANPROJ_8: 75

      .= 3 by A2, A5, EUCLID_8: 50;

      

       A7: ( width N) = 3 by MATRIX_0: 24

      .= ( len ( <*pf*> @ )) by MATRIX_0:def 6, A6;

      (N * ( <*pf*> @ )) is Matrix of 3, 1, F_Real by A2, FINSEQ_3: 153, ANPROJ_8: 91;

      then

       A8: [1, 1] in ( Indices (N * ( <*pf*> @ ))) & [2, 1] in ( Indices (N * ( <*pf*> @ ))) & [3, 1] in ( Indices (N * ( <*pf*> @ ))) by MATRIX_0: 23, ANPROJ_8: 2;

      

       A9: i = 1 or ... or i = 3 by A1, FINSEQ_1: 91;

      ((N * pf) . i) = ((N * ( <*pf*> @ )) . i) by LAPLACE:def 9

      .= ( Line ((N * ( <*pf*> @ )),i)) by A1, A3, MATRIX_0: 52

      .= <*((N * ( <*pf*> @ )) * (i,1))*> by A9, A4, ANPROJ_8: 92;

      

      then (((N * pf) . i) . 1) = ((N * ( <*pf*> @ )) * (i,1)) by FINSEQ_1: 40

      .= (( Line (N,i)) "*" ( Col (( <*pf*> @ ),1))) by A9, A7, A8, MATRIX_3:def 4;

      hence thesis by ANPROJ_8: 93;

    end;

    registration

      let n be Nat;

      cluster ( 1. ( F_Real ,n)) -> invertible;

      coherence ;

    end

    registration

      let n be Nat;

      let M be invertible Matrix of n, F_Real ;

      cluster (M ~ ) -> invertible;

      coherence ;

    end

    registration

      let n be Nat;

      let K be Field;

      let N1,N2 be invertible Matrix of n, K;

      cluster (N1 * N2) -> invertible;

      coherence by MATRIX_6: 36;

    end

    begin

    reserve N,N1,N2 for invertible Matrix of 3, F_Real ;

    reserve P,P1,P2,P3 for Point of ( ProjectiveSpace ( TOP-REAL 3));

    theorem :: ANPROJ_9:13

    

     Th14: (( homography N1) . (( homography N2) . P)) = (( homography (N1 * N2)) . P)

    proof

      consider u12,v12 be Element of ( TOP-REAL 3), u12f be FinSequence of F_Real , p12 be 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 be Element of ( TOP-REAL 3), u2f be FinSequence of F_Real , p2 be 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 be Element of ( TOP-REAL 3), u1f be FinSequence of F_Real , p1 be 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 be 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 be 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))*>

      proof

        (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)) by FINSEQ_1: 40;

        hence thesis by A19, A27, A18, ANPROJ_8:def 2;

      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)) by FINSEQ_1: 40;

        hence thesis by A12, A31, A11, ANPROJ_8:def 2;

      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)) by FINSEQ_1: 40;

        hence thesis by A5, A36, A4, ANPROJ_8:def 2;

      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 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, FINSEQ_1: 45;

      reconsider t1 = (v2f . 1), t2 = (v2f . 2), t3 = (v2f . 3) as Element of F_Real by A32, FINSEQ_1: 45;

      ( 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, FINSEQ_1: 45

      .= (( 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, FINSEQ_1: 45

      .= (( 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, FINSEQ_1: 45

      .= (( Line (N2,3)) "*" ( Col (( <*u2f*> @ ),1))) by A30, A47, MATRIX_3:def 4

      .= (( Line (N2,3)) "*" u2f) by ANPROJ_8: 93;

      now

        ( 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;

        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;

      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, FINSEQ_1: 45;

      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

          ( 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;

          ( 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;

        end;

        hence thesis by FINSEQ_1: 45;

      end;

      ( Dir v1) = ( Dir v12)

      proof

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

        proof

          set c = (a * b);

          take c;

          thus c <> 0 by A22, A24, XCMPLX_1: 6;

           A61:

          now

            thus ((N1 * ( <*u1f*> @ )) * (1,1)) = (c * (((N1 * N2) * ( <*u12f*> @ )) * (1,1)))

            proof

              (v1 . 1) = (c * (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, FINSEQ_1: 45

                .= (( 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

                  

                  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;

                  

                  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;

                  

                  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;

                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, FINSEQ_1: 45;

                hence thesis;

              end;

              hence thesis by A45, A37, FINSEQ_1: 45;

            end;

            thus ((N1 * ( <*u1f*> @ )) * (2,1)) = (c * (((N1 * N2) * ( <*u12f*> @ )) * (2,1)))

            proof

              (v1 . 2) = (c * (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, FINSEQ_1: 45

                .= (( 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

                  

                  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;

                  

                  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;

                  

                  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;

                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, FINSEQ_1: 45;

                hence thesis;

              end;

              hence thesis by A45, A37, FINSEQ_1: 45;

            end;

            thus ((N1 * ( <*u1f*> @ )) * (3,1)) = (c * (((N1 * N2) * ( <*u12f*> @ )) * (3,1)))

            proof

              (v1 . 3) = (c * (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, FINSEQ_1: 45

                .= (( 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

                  

                  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;

                  

                  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;

                  

                  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;

                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, FINSEQ_1: 45;

                hence thesis;

              end;

              hence thesis by A45, A37, FINSEQ_1: 45;

            end;

          end;

           <*(c * (((N1 * N2) * ( <*u12f*> @ )) * (1,1))), (c * (((N1 * N2) * ( <*u12f*> @ )) * (2,1))), (c * (((N1 * N2) * ( <*u12f*> @ )) * (3,1)))*> = (c * |[(((N1 * N2) * ( <*u12f*> @ )) * (1,1)), (((N1 * N2) * ( <*u12f*> @ )) * (2,1)), (((N1 * N2) * ( <*u12f*> @ )) * (3,1))]|) by EUCLID_5: 8

          .= (c * <*(((N1 * N2) * ( <*u12f*> @ )) * (1,1)), (((N1 * N2) * ( <*u12f*> @ )) * (2,1)), (((N1 * N2) * ( <*u12f*> @ )) * (3,1))*>);

          hence thesis by A28, A37, A61;

        end;

        then are_Prop (v1,v12) by ANPROJ_1: 1;

        hence thesis by A6, A20, ANPROJ_1: 22;

      end;

      hence thesis by A7, A21;

    end;

    theorem :: ANPROJ_9:14

    

     Th15: (( homography ( 1. ( F_Real ,3))) . P) = P

    proof

      consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be 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 thesis by A1, A3, A5, A7, A9, ANPROJ_8: 86;

    end;

    theorem :: ANPROJ_9:15

    

     Th16: (( homography N) . (( homography (N ~ )) . P)) = P & (( homography (N ~ )) . (( homography N) . P)) = P

    proof

      

       A1: (N ~ ) is_reverse_of N by MATRIX_6:def 4;

      

      thus (( homography N) . (( homography (N ~ )) . P)) = (( homography (N * (N ~ ))) . P) by Th14

      .= (( homography ( 1. ( F_Real ,3))) . P) by A1, MATRIX_6:def 2

      .= P by Th15;

      

      thus (( homography (N ~ )) . (( homography N) . P)) = (( homography ((N ~ ) * N)) . P) by Th14

      .= (( homography ( 1. ( F_Real ,3))) . P) by A1, MATRIX_6:def 2

      .= P by Th15;

    end;

    theorem :: ANPROJ_9:16

    (( homography N) . P1) = (( homography N) . P2) implies P1 = P2

    proof

      assume

       A1: (( homography N) . P1) = (( homography N) . P2);

      P1 = (( homography (N ~ )) . (( homography N) . P1)) by Th16

      .= P2 by A1, Th16;

      hence thesis;

    end;

    

     Lem06: ( len uf) = 3 implies ((a * ( 1. ( F_Real ,3))) * ( <*uf*> @ )) = (a * ( <*uf*> @ ))

    proof

      assume

       A1: ( len uf) = 3;

      ( width <*uf*>) = 3 by A1, MATRIX_0: 23;

      then ( len ( <*uf*> @ )) = 3 by MATRIX_0: 29;

      then ( width ( 1. ( F_Real ,3))) = ( len ( <*uf*> @ )) by MATRIX_0: 23;

      then ((a * ( 1. ( F_Real ,3))) * ( <*uf*> @ )) = (a * (( 1. ( F_Real ,3)) * ( <*uf*> @ ))) by MATRIX15: 1;

      hence thesis by A1, ANPROJ_8: 99;

    end;

    theorem :: ANPROJ_9:17

    

     Th17: for a be non zero Element of F_Real st (a * ( 1. ( F_Real ,3))) = N holds (( homography N) . P) = P

    proof

      let a be non zero Element of F_Real ;

      assume

       A1: (a * ( 1. ( F_Real ,3))) = N;

      set aN = N;

      consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be 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 = (aN * uf) and

       A6: v = ( M2F p) and

       A7: not v is zero and

       A8: (( homography aN) . P) = ( Dir v) by ANPROJ_8:def 4;

      u in ( TOP-REAL 3);

      then

       A9: uf in ( REAL 3) by A4, EUCLID: 22;

      

       A10: (aN * ( <*uf*> @ )) is Matrix of 3, 1, F_Real by A4, FINSEQ_3: 153, ANPROJ_8: 91;

      p = (aN * ( <*uf*> @ )) by A5, LAPLACE:def 9;

      then

       A11: ( len p) = 3 by A10, MATRIX_0: 23;

      

       A12: p = (aN * ( <*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

        (( 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, FINSEQ_1: 45

        .= (uf . 1) by FINSEQ_1:def 8;

        hence (((a * ( <*uf*> @ )) . 1) . 1) = (a * (u . 1)) by A4, A20, MATRPROB: 14, A16;

        (( <*uf*> @ ) * (2,1)) = ((( <*uf*> @ ) . 2) . 1) by A15, MATRPROB: 14

        .= ( <*(uf . 2)*> . 1) by A17, FINSEQ_1: 45

        .= (uf . 2) by FINSEQ_1:def 8;

        hence (((a * ( <*uf*> @ )) . 2) . 1) = (a * (u . 2)) by A4, A20, MATRPROB: 14, A16;

        (( <*uf*> @ ) * (3,1)) = ((( <*uf*> @ ) . 3) . 1) by A15, MATRPROB: 14

        .= ( <*(uf . 3)*> . 1) by A17, FINSEQ_1: 45

        .= (uf . 3) by FINSEQ_1:def 8;

        hence (((a * ( <*uf*> @ )) . 3) . 1) = (a * (u . 3)) by A4, A20, MATRPROB: 14, A16;

      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;

      a is non zero;

      then are_Prop (v,u) by A21, ANPROJ_1: 1;

      hence thesis by A2, A3, A7, A8, ANPROJ_1: 22;

    end;

    definition

      :: ANPROJ_9:def1

      func EnsHomography3 -> set equals the set of all ( homography N) where N be invertible Matrix of 3, F_Real ;

      coherence ;

    end

    registration

      cluster EnsHomography3 -> non empty;

      coherence

      proof

        ( homography ( 1. ( F_Real ,3))) in EnsHomography3 ;

        hence thesis;

      end;

    end

    definition

      let h1,h2 be Element of EnsHomography3 ;

      :: ANPROJ_9:def2

      func h1 (*) h2 -> Element of EnsHomography3 means

      : Def01: ex N1,N2 be invertible Matrix of 3, F_Real st h1 = ( homography N1) & h2 = ( homography N2) & it = ( homography (N1 * N2));

      existence

      proof

        h1 in the set of all ( homography N) where N be invertible Matrix of 3, F_Real ;

        then

        consider N1 be invertible Matrix of 3, F_Real such that

         A1: h1 = ( homography N1);

        h2 in the set of all ( homography N) where N be invertible Matrix of 3, F_Real ;

        then

        consider N2 be invertible Matrix of 3, F_Real such that

         A2: h2 = ( homography N2);

        ( homography (N1 * N2)) in EnsHomography3 ;

        hence thesis by A1, A2;

      end;

      uniqueness

      proof

        let H1,H2 be Element of EnsHomography3 such that

         A3: ex N1,N2 be invertible Matrix of 3, F_Real st h1 = ( homography N1) & h2 = ( homography N2) & H1 = ( homography (N1 * N2)) and

         A4: ex N1,N2 be invertible Matrix of 3, F_Real st h1 = ( homography N1) & h2 = ( homography N2) & H2 = ( homography (N1 * N2));

        consider NA1,NA2 be invertible Matrix of 3, F_Real such that

         A5: h1 = ( homography NA1) and

         A6: h2 = ( homography NA2) and

         A7: H1 = ( homography (NA1 * NA2)) by A3;

        consider NB1,NB2 be invertible Matrix of 3, F_Real such that

         A8: h1 = ( homography NB1) and

         A9: h2 = ( homography NB2) and

         A10: H2 = ( homography (NB1 * NB2)) by A4;

        reconsider fH1 = H1, fH2 = H2 as Function of ( ProjectiveSpace ( TOP-REAL 3)), ( ProjectiveSpace ( TOP-REAL 3)) by A7, A10;

        now

          ( dom fH1) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

          hence ( dom fH1) = ( dom fH2) by FUNCT_2:def 1;

          thus for x be object st x in ( dom fH1) holds (fH1 . x) = (fH2 . x)

          proof

            let x be object;

            assume x in ( dom fH1);

            then

            reconsider P = x as Element of ( ProjectiveSpace ( TOP-REAL 3));

            (fH1 . x) = (( homography NB1) . (( homography NB2) . P)) by A5, A6, A7, A8, A9, Th14

            .= (fH2 . x) by A10, Th14;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

    end

    theorem :: ANPROJ_9:18

    

     Th18: for h1,h2 be Element of EnsHomography3 st h1 = ( homography N1) & h2 = ( homography N2) holds ( homography (N1 * N2)) = (h1 (*) h2)

    proof

      let h1,h2 be Element of EnsHomography3 ;

      assume that

       A1: h1 = ( homography N1) and

       A2: h2 = ( homography N2);

      consider M1,M2 be invertible Matrix of 3, F_Real such that

       A3: h1 = ( homography M1) and

       A4: h2 = ( homography M2) and

       A5: (h1 (*) h2) = ( homography (M1 * M2)) by Def01;

      reconsider h12 = (h1 (*) h2) as Function of ( ProjectiveSpace ( TOP-REAL 3)), ( ProjectiveSpace ( TOP-REAL 3)) by A5;

      now

        ( dom ( homography (N1 * N2))) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

        hence ( dom ( homography (N1 * N2))) = ( dom h12) by FUNCT_2:def 1;

        thus for x be object st x in ( dom ( homography (N1 * N2))) holds (( homography (N1 * N2)) . x) = (h12 . x)

        proof

          let x be object;

          assume x in ( dom ( homography (N1 * N2)));

          then

          reconsider xf = x as Element of ( ProjectiveSpace ( TOP-REAL 3));

          (( homography (N1 * N2)) . xf) = (( homography N1) . (( homography N2) . xf)) by Th14

          .= (h12 . xf) by A3, A4, A5, A1, A2, Th14;

          hence thesis;

        end;

      end;

      hence thesis by FUNCT_1:def 11;

    end;

    theorem :: ANPROJ_9:19

    

     Ta1: for x,y,z be Element of EnsHomography3 holds ((x (*) y) (*) z) = (x (*) (y (*) z))

    proof

      let x,y,z be Element of EnsHomography3 ;

      x in EnsHomography3 ;

      then

      consider Nx be invertible Matrix of 3, F_Real such that

       A2: x = ( homography Nx);

      y in EnsHomography3 ;

      then

      consider Ny be invertible Matrix of 3, F_Real such that

       A3: y = ( homography Ny);

      z in EnsHomography3 ;

      then

      consider Nz be invertible Matrix of 3, F_Real such that

       A4: z = ( homography Nz);

      

       A5: ( width Nx) = 3 & ( len Ny) = 3 & ( width Ny) = 3 & ( len Nz) = 3 by MATRIX_0: 24;

      (y (*) z) = ( homography (Ny * Nz)) by A3, A4, Th18;

      

      then

       A6: (x (*) (y (*) z)) = ( homography (Nx * (Ny * Nz))) by A2, Th18

      .= ( homography ((Nx * Ny) * Nz)) by A5, MATRIX_3: 33;

      (x (*) y) = ( homography (Nx * Ny)) by A2, A3, Th18;

      hence thesis by A6, A4, Th18;

    end;

    definition

      :: ANPROJ_9:def3

      func BinOpHomography3 -> BinOp of EnsHomography3 means

      : Def02: for h1,h2 be Element of EnsHomography3 holds (it . (h1,h2)) = (h1 (*) h2);

      existence from BINOP_1:sch 4;

      uniqueness from BINOP_2:sch 2;

    end

    definition

      :: ANPROJ_9:def4

      func GroupHomography3 -> strict multMagma equals multMagma (# EnsHomography3 , BinOpHomography3 #);

      coherence ;

    end

    set GH3 = GroupHomography3 ;

     Lm1:

    now

      let e be Element of GH3 such that

       A1: e = ( homography ( 1. ( F_Real ,3)));

      let h be Element of GH3;

      reconsider h1 = h, h2 = e as Element of EnsHomography3 ;

      consider N1,N2 be invertible Matrix of 3, F_Real such that

       A10: h1 = ( homography N1) and

       A11: h2 = ( homography N2) and

       A12: (h1 (*) h2) = ( homography (N1 * N2)) by Def01;

      ( homography (N1 * N2)) = ( homography N1)

      proof

        ( dom ( homography (N1 * N2))) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

        then

         A14: ( dom ( homography (N1 * N2))) = ( dom ( homography N1)) by FUNCT_2:def 1;

        for x be object st x in ( dom ( homography N1)) holds (( homography (N1 * N2)) . x) = (( homography N1) . x)

        proof

          let x be object;

          assume x in ( dom ( homography N1));

          then

          reconsider xf = x as Point of ( ProjectiveSpace ( TOP-REAL 3));

          (( homography (N1 * N2)) . xf) = (( homography N1) . (( homography N2) . xf)) by Th14

          .= (( homography N1) . xf) by A1, A11, Th15;

          hence thesis;

        end;

        hence thesis by A14, FUNCT_1:def 11;

      end;

      hence (h * e) = h by Def02, A10, A12;

      consider N2,N1 be invertible Matrix of 3, F_Real such that

       A15: h2 = ( homography N2) and

       A16: h1 = ( homography N1) and

       A17: (h2 (*) h1) = ( homography (N2 * N1)) by Def01;

      ( homography (N2 * N1)) = ( homography N1)

      proof

        ( dom ( homography (N2 * N1))) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

        then

         A18: ( dom ( homography (N2 * N1))) = ( dom ( homography N1)) by FUNCT_2:def 1;

        for x be object st x in ( dom ( homography N1)) holds (( homography (N2 * N1)) . x) = (( homography N1) . x)

        proof

          let x be object;

          assume x in ( dom ( homography N1));

          then

          reconsider xf = x as Point of ( ProjectiveSpace ( TOP-REAL 3));

          (( homography (N2 * N1)) . xf) = (( homography N2) . (( homography N1) . xf)) by Th14

          .= (( homography N1) . xf) by A1, A15, Th15;

          hence thesis;

        end;

        hence thesis by A18, FUNCT_1:def 11;

      end;

      hence (e * h) = h by Def02, A16, A17;

    end;

     Lm2:

    now

      let e,h,g be Element of GH3;

      let N,Ng be invertible Matrix of 3, F_Real such that

       A9: h = ( homography N) and

       B1: g = ( homography Ng) and

       B2: Ng = (N ~ ) and

       B3: e = ( homography ( 1. ( F_Real ,3)));

      reconsider h1 = h as Element of EnsHomography3 ;

      

       A23: Ng is_reverse_of N by B2, MATRIX_6:def 4;

      reconsider g1 = g as Element of EnsHomography3 ;

      consider N1,N2 be invertible Matrix of 3, F_Real such that

       A19: h1 = ( homography N1) and

       A20: g1 = ( homography N2) and

       A21: (h1 (*) g1) = ( homography (N1 * N2)) by Def01;

      ( homography (N1 * N2)) = ( homography (N * Ng))

      proof

        now

          ( dom ( homography (N1 * N2))) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

          hence ( dom ( homography (N1 * N2))) = ( dom ( homography (N * Ng))) by FUNCT_2:def 1;

          thus for x be object st x in ( dom ( homography (N1 * N2))) holds (( homography (N1 * N2)) . x) = (( homography (N * Ng)) . x)

          proof

            let x be object;

            assume x in ( dom ( homography (N1 * N2)));

            then

            reconsider xf = x as Point of ( ProjectiveSpace ( TOP-REAL 3));

            (( homography (N1 * N2)) . xf) = (( homography N) . (( homography Ng) . xf)) by Th14, A19, A9, A20, B1

            .= (( homography (N * Ng)) . xf) by Th14;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

      then (h1 (*) g1) = e by B3, A21, A23, MATRIX_6:def 2;

      hence (h * g) = e by Def02;

      consider N1,N2 be invertible Matrix of 3, F_Real such that

       A27: g1 = ( homography N1) and

       A28: h1 = ( homography N2) and

       A29: (g1 (*) h1) = ( homography (N1 * N2)) by Def01;

      ( homography (N1 * N2)) = ( homography (Ng * N))

      proof

        now

          ( dom ( homography (N1 * N2))) = the carrier of ( ProjectiveSpace ( TOP-REAL 3)) by FUNCT_2:def 1;

          hence ( dom ( homography (N1 * N2))) = ( dom ( homography (Ng * N))) by FUNCT_2:def 1;

          thus for x be object st x in ( dom ( homography (N1 * N2))) holds (( homography (N1 * N2)) . x) = (( homography (Ng * N)) . x)

          proof

            let x be object;

            assume x in ( dom ( homography (N1 * N2)));

            then

            reconsider xf = x as Point of ( ProjectiveSpace ( TOP-REAL 3));

            (( homography (N1 * N2)) . xf) = (( homography Ng) . (( homography N) . xf)) by Th14, A27, A9, A28, B1

            .= (( homography (Ng * N)) . xf) by Th14;

            hence thesis;

          end;

        end;

        hence thesis by FUNCT_1:def 11;

      end;

      then (g1 (*) h1) = e by A29, A23, B3, MATRIX_6:def 2;

      hence (g * h) = e by Def02;

    end;

    set e = ( homography ( 1. ( F_Real ,3)));

    e in EnsHomography3 ;

    then

    reconsider e as Element of GH3;

    registration

      cluster GroupHomography3 -> non empty associative Group-like;

      coherence

      proof

        thus GH3 is non empty;

        thus GH3 is associative

        proof

          let x,y,z be Element of GH3;

          reconsider xf = x, yf = y, zf = z as Element of EnsHomography3 ;

          

           A7: (x * y) = (xf (*) yf) by Def02;

          

           A8: ((x * y) * z) = ((xf (*) yf) (*) zf) by Def02, A7;

          (y * z) = (yf (*) zf) by Def02;

          then (x * (y * z)) = (xf (*) (yf (*) zf)) by Def02;

          hence thesis by A8, Ta1;

        end;

        take e;

        let h be Element of GH3;

        thus (h * e) = h & (e * h) = h by Lm1;

        h in EnsHomography3 ;

        then

        consider N be invertible Matrix of 3, F_Real such that

         A9: h = ( homography N);

        reconsider Ng = (N ~ ) as invertible Matrix of 3, F_Real ;

        ( homography Ng) in EnsHomography3 ;

        then

        reconsider g = ( homography Ng) as Element of GH3;

        take g;

        thus thesis by A9, Lm2;

      end;

    end

    theorem :: ANPROJ_9:20

    

     Ta2: ( 1_ GroupHomography3 ) = ( homography ( 1. ( F_Real ,3)))

    proof

      for h be Element of GH3 holds (h * e) = h & (e * h) = h by Lm1;

      hence thesis by GROUP_1: 4;

    end;

    theorem :: ANPROJ_9:21

    for h,g be Element of GroupHomography3 holds for N,Ng be invertible Matrix of 3, F_Real st h = ( homography N) & g = ( homography Ng) & Ng = (N ~ ) holds g = (h " )

    proof

      let h,g be Element of GH3;

      let N,Ng be invertible Matrix of 3, F_Real ;

      assume h = ( homography N) & g = ( homography Ng) & Ng = (N ~ );

      then (h * g) = ( 1_ GH3) & (g * h) = ( 1_ GH3) by Lm2, Ta2;

      hence g = (h " ) by GROUP_1:def 5;

    end;

    begin

    definition

      :: ANPROJ_9:def5

      func Dir100 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[1, 0 , 0 ]|);

      coherence by Th11, ANPROJ_1: 26;

      :: ANPROJ_9:def6

      func Dir010 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[ 0 , 1, 0 ]|);

      coherence by Th11, ANPROJ_1: 26;

      :: ANPROJ_9:def7

      func Dir001 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[ 0 , 0 , 1]|);

      coherence by Th11, ANPROJ_1: 26;

      :: ANPROJ_9:def8

      func Dir111 -> Point of ( ProjectiveSpace ( TOP-REAL 3)) equals ( Dir |[1, 1, 1]|);

      coherence by Th11, ANPROJ_1: 26;

    end

    theorem :: ANPROJ_9:22

     Dir100 <> Dir010 & Dir100 <> Dir001 & Dir100 <> Dir111 & Dir010 <> Dir001 & Dir010 <> Dir111 & Dir001 <> Dir111

    proof

      assume

       A1: Dir100 = Dir010 or Dir100 = Dir001 or Dir100 = Dir111 or Dir010 = Dir001 or Dir010 = Dir111 or Dir001 = Dir111 ;

      consider u100 be Element of ( TOP-REAL 3) such that

       A2: u100 = |[1, 0 , 0 ]| and

       A3: Dir100 = ( Dir u100);

      consider u010 be Element of ( TOP-REAL 3) such that

       A4: u010 = |[ 0 , 1, 0 ]| and

       A5: Dir010 = ( Dir u010);

      consider u001 be Element of ( TOP-REAL 3) such that

       A6: u001 = |[ 0 , 0 , 1]| and

       A7: Dir001 = ( Dir u001);

      consider u111 be Element of ( TOP-REAL 3) such that

       A8: u111 = |[1, 1, 1]| and

       A9: Dir111 = ( Dir u111);

      per cases by A1;

        suppose

         A10: Dir100 = Dir010 ;

         not u100 is zero & not u010 is zero by A2, A4, EUCLID_5: 4, FINSEQ_1: 78;

        then are_Prop (u100,u010) by A3, A5, A10, ANPROJ_1: 22;

        then

        consider a be Real such that a <> 0 and

         A12: u100 = (a * u010) by ANPROJ_1: 1;

         |[1, 0 , 0 ]| = |[(a * 0 ), (a * 1), 0 ]| by A2, A4, A12, EUCLID_5: 8

        .= |[ 0 , a, 0 ]|;

        then 1 = ( |[ 0 , a, 0 ]| `1 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

        suppose

         A13: Dir100 = Dir001 ;

         not u100 is zero & not u001 is zero by A2, A6, EUCLID_5: 4, FINSEQ_1: 78;

        then are_Prop (u100,u001) by A13, A3, A7, ANPROJ_1: 22;

        then

        consider a be Real such that a <> 0 and

         A15: u100 = (a * u001) by ANPROJ_1: 1;

         |[1, 0 , 0 ]| = |[(a * 0 ), (a * 0 ), (a * 1)]| by A2, A6, A15, EUCLID_5: 8

        .= |[ 0 , 0 , a]|;

        then 1 = ( |[ 0 , 0 , a]| `1 ) by EUCLID_5: 2;

        hence thesis by EUCLID_5: 2;

      end;

        suppose

         A16: Dir100 = Dir111 ;

         not u100 is zero & not u111 is zero by A2, A8, EUCLID_5: 4, FINSEQ_1: 78;

        then are_Prop (u100,u111) by A16, A3, A9, ANPROJ_1: 22;

        then

        consider a be Real such that

         A17: a <> 0 and

         A18: u100 = (a * u111) by ANPROJ_1: 1;

         |[1, 0 , 0 ]| = |[(a * 1), (a * 1), (a * 1)]| by A2, A8, A18, EUCLID_5: 8

        .= |[a, a, a]|;

        then 0 = ( |[a, a, a]| `2 ) by EUCLID_5: 2;

        hence thesis by A17, EUCLID_5: 2;

      end;

        suppose

         A19: Dir010 = Dir001 ;

         not u010 is zero & not u001 is zero by A4, A6, EUCLID_5: 4, FINSEQ_1: 78;

        then are_Prop (u010,u001) by A5, A7, A19, ANPROJ_1: 22;

        then

        consider a be Real such that

         A20: a <> 0 and

         A21: u010 = (a * u001) by ANPROJ_1: 1;

         |[ 0 , 1, 0 ]| = |[(a * 0 ), (a * 0 ), (a * 1)]| by A4, A6, A21, EUCLID_5: 8

        .= |[ 0 , 0 , a]|;

        then 0 = ( |[ 0 , 0 , a]| `3 ) by EUCLID_5: 2;

        hence thesis by A20, EUCLID_5: 2;

      end;

        suppose

         A22: Dir010 = Dir111 ;

         not u010 is zero & not u111 is zero by A4, A8, EUCLID_5: 4, FINSEQ_1: 78;

        then are_Prop (u010,u111) by A22, A5, A9, ANPROJ_1: 22;

        then

        consider a be Real such that

         A23: a <> 0 and

         A24: u010 = (a * u111) by ANPROJ_1: 1;

         |[ 0 , 1, 0 ]| = |[(a * 1), (a * 1), a]| by A4, A8, A24, EUCLID_5: 8

        .= |[a, a, a]|;

        then 0 = ( |[a, a, a]| `1 ) by EUCLID_5: 2;

        hence thesis by A23, EUCLID_5: 2;

      end;

        suppose

         A25: Dir001 = Dir111 ;

         not u001 is zero & not u111 is zero by A6, A8, EUCLID_5: 4, FINSEQ_1: 78;

        then are_Prop (u001,u111) by A7, A9, A25, ANPROJ_1: 22;

        then

        consider a be Real such that

         A26: a <> 0 and

         A27: u001 = (a * u111) by ANPROJ_1: 1;

         |[ 0 , 0 , 1]| = |[(a * 1), (a * 1), a]| by A6, A8, A27, EUCLID_5: 8

        .= |[a, a, a]|;

        then 0 = ( |[a, a, a]| `1 ) by EUCLID_5: 2;

        hence thesis by A26, EUCLID_5: 2;

      end;

    end;

    registration

      let a be non zero Element of F_Real ;

      let N;

      cluster (a * N) -> invertible;

      coherence

      proof

        consider N2 be Matrix of 3, F_Real such that

         A1: N is_reverse_of N2 by MATRIX_6:def 3;

        reconsider b = (1 / a) as Element of F_Real by XREAL_0:def 1;

        

         A2: ( 1_ F_Real ) = ( 1. F_Real );

        a is non zero;

        

        then

         A3: ((b * a) * (N2 * N)) = (( 1. F_Real ) * (N2 * N)) by XCMPLX_1: 106

        .= (N2 * N) by A2, MATRIX15: 2;

        now

          

           A4: ( width N2) = 3 & ( width N) = 3 by MATRIX_0: 23;

          then

           A5: ( width N2) = ( len N) & ( width N) = ( len N2) by MATRIX_0: 23;

          

           A6: ( width N2) = ( len (a * N)) & ( width N) = ( len (b * N2)) by A4, MATRIX_0: 23;

          

          hence ((b * N2) * (a * N)) = (b * (N2 * (a * N))) by MATRIX15: 1

          .= (b * (a * (N2 * N))) by A5, MATRIXR1: 22

          .= ((b * a) * (N2 * N)) by MATRIX15: 2

          .= ((a * b) * (N * N2)) by A1, MATRIX_6:def 2

          .= (a * (b * (N * N2))) by MATRIX15: 2

          .= (a * (N * (b * N2))) by A5, MATRIXR1: 22

          .= ((a * N) * (b * N2)) by A6, MATRIX15: 1;

          

          thus ((b * N2) * (a * N)) = (b * (N2 * (a * N))) by A6, MATRIX15: 1

          .= (b * (a * (N2 * N))) by A5, MATRIXR1: 22

          .= (N2 * N) by A3, MATRIX15: 2

          .= ( 1. ( F_Real ,3)) by A1, MATRIX_6:def 2;

        end;

        hence thesis by MATRIX_6:def 2, MATRIX_6:def 3;

      end;

    end

    theorem :: ANPROJ_9:23

    for a be non zero Element of F_Real holds (( homography (a * N1)) . P) = (( homography N1) . P)

    proof

      let a be non zero Element of F_Real ;

      set M = (a * ( 1. ( F_Real ,3)));

      

      thus (( homography (a * N1)) . P) = (( homography (M * N1)) . P) by Th02

      .= (( homography M) . (( homography N1) . P)) by Th14

      .= (( homography N1) . P) by Th17;

    end;

    theorem :: ANPROJ_9:24

    

     Th20: not (P1,P2,P3) are_collinear implies ex N be invertible Matrix of 3, F_Real st (( homography N) . P1) = Dir100 & (( homography N) . P2) = Dir010 & (( homography N) . P3) = Dir001

    proof

      assume

       A1: not (P1,P2,P3) are_collinear ;

      consider u1 be Element of ( TOP-REAL 3) such that

       A2: not u1 is zero and

       A3: P1 = ( Dir u1) by ANPROJ_1: 26;

      consider u2 be Element of ( TOP-REAL 3) such that

       A4: not u2 is zero and

       A5: P2 = ( Dir u2) by ANPROJ_1: 26;

      consider u3 be 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 be 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 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;

      thus (( homography N) . P1) = Dir100

      proof

        consider nu1,nv1 be Element of ( TOP-REAL 3), u1f be FinSequence of F_Real , p1 be 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 be 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, FINSEQ_1: 45;

        

         A29: (((N * pf) . 1) . 1) = ( |[1, 0 , 0 ]| . 1) by A28, FINSEQ_1: 40, 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, FINSEQ_1: 40, 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, FINSEQ_1: 40, 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 be 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

            thus ( len (N * pf)) = 3 by A10, A13, ANPROJ_8: 78;

            thus ((N * pf) . 1) = <*(a * pp1)*>

            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 thesis by A34, FINSEQ_1: 40;

            end;

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

            proof

              (( Line (N,2)) "*" pf) = (((N * pf) . 2) . 1) by FINSEQ_1: 1, Lem05;

              hence thesis by A35, FINSEQ_1: 40, A28, A30, A32;

            end;

            (( Line (N,3)) "*" pf) = (((N * pf) . 3) . 1) by FINSEQ_1: 1, Lem05;

            hence ((N * pf) . 3) = <*(a * pp3)*> by A36, FINSEQ_1: 40, A28, A32, A31;

          end;

          hence thesis by A37, FINSEQ_1: 45;

        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;

        nv1 is non zero & (a * nv1) is non zero & are_Prop (nv1,(a * nv1)) by A19, A21, Th04, ANPROJ_1: 1;

        hence thesis by A38, EUCLID_8:def 1, ANPROJ_1: 22, A20;

      end;

      thus (( homography N) . P2) = Dir010

      proof

        consider nu2,nv2 be Element of ( TOP-REAL 3), u2f be FinSequence of F_Real , p2 be 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 be 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, FINSEQ_1: 45;

        

         A54: (((N * qf) . 1) . 1) = ( |[ 0 , 1, 0 ]| . 1) by A53, FINSEQ_1: 40, 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, FINSEQ_1: 40, 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, FINSEQ_1: 40, 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 be 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

            thus ( len (N * qf)) = 3 by A11, A13, ANPROJ_8: 78;

            (( Line (N,1)) "*" qf) = (((N * qf) . 1) . 1) by FINSEQ_1: 1, Lem05;

            hence ((N * qf) . 1) = <*(a * pp1)*> by A59, FINSEQ_1: 40, A53, A57, A54;

            thus ((N * qf) . 2) = <*(a * pp2)*>

            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 thesis by A60, FINSEQ_1: 40;

            end;

            (( Line (N,3)) "*" qf) = (((N * qf) . 3) . 1) by FINSEQ_1: 1, Lem05;

            hence ((N * qf) . 3) = <*(a * pp3)*> by A61, FINSEQ_1: 40, A53, A57, A56;

          end;

          hence thesis by A62, FINSEQ_1: 45;

        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;

        nv2 is non zero & (a * nv2) is non zero & are_Prop (nv2,(a * nv2)) by A44, A46, Th04, ANPROJ_1: 1;

        hence thesis by A63, EUCLID_8:def 2, ANPROJ_1: 22, A45;

      end;

      thus (( homography N) . P3) = Dir001

      proof

        consider nu3,nv3 be Element of ( TOP-REAL 3), u3f be FinSequence of F_Real , p3 be 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 be 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, FINSEQ_1: 45;

        

         A79: (((N * rf) . 1) . 1) = ( |[ 0 , 0 , 1]| . 1) by A78, FINSEQ_1: 40, 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, FINSEQ_1: 40, 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, FINSEQ_1: 40, 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 be 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

            thus ( len (N * rf)) = 3 by A12, A13, ANPROJ_8: 78;

            (( Line (N,1)) "*" rf) = (((N * rf) . 1) . 1) by FINSEQ_1: 1, Lem05;

            hence ((N * rf) . 1) = <*(a * pp1)*> by A84, FINSEQ_1: 40, A78, A82, A79;

            (( Line (N,2)) "*" rf) = (((N * rf) . 2) . 1) by FINSEQ_1: 1, Lem05;

            hence ((N * rf) . 2) = <*(a * pp2)*> by A85, FINSEQ_1: 40, A78, A82, A80;

            thus ((N * rf) . 3) = <*(a * pp3)*>

            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 thesis by A86, FINSEQ_1: 40;

            end;

          end;

          hence thesis by A87, FINSEQ_1: 45;

        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;

        nv3 is non zero & (a * nv3) is non zero & are_Prop (nv3,(a * nv3)) by A69, A71, Th04, ANPROJ_1: 1;

        hence thesis by A88, EUCLID_8:def 3, ANPROJ_1: 22, A70;

      end;

    end;

    theorem :: ANPROJ_9:25

    

     Th21: for a,b,c be non zero Element of F_Real st N = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> holds (( homography N) . Dir100 ) = Dir100 & (( homography N) . Dir010 ) = Dir010 & (( homography N) . Dir001 ) = Dir001

    proof

      let a,b,c be non zero Element of F_Real ;

      assume

       A1: N = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*>;

      thus (( homography N) . Dir100 ) = Dir100

      proof

        consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be FinSequence of (1 -tuples_on REAL ) such that

         A2: Dir100 = ( 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) . Dir100 ) = ( Dir v) by ANPROJ_8:def 4;

         not |[1, 0 , 0 ]| is zero by EUCLID_8:def 1, Th13;

        then are_Prop (u, |[1, 0 , 0 ]|) by A2, A3, ANPROJ_1: 22;

        then

        consider d be Real such that d <> 0 and

         A9: u = (d * |[1, 0 , 0 ]|) by ANPROJ_1: 1;

        

         A10: u = |[(d * 1), (d * 0 ), (d * 0 )]| by A9, EUCLID_5: 8

        .= |[d, 0 , 0 ]|;

        then (u `1 ) = d & (u `2 ) = 0 & (u `3 ) = 0 by EUCLID_5: 2;

        then

         A11: (uf . 1) = d & (uf . 2) = 0 & (uf . 3) = 0 by A4, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

        u in ( TOP-REAL 3);

        then u in ( REAL 3) by EUCLID: 22;

        then

         A12: ( <*uf*> @ ) = <* <*d*>, <* 0 *>, <* 0 *>*> by A11, A4, EUCLID_8: 50, ANPROJ_8: 77;

        then

        reconsider Mu = ( <*uf*> @ ) as Matrix of 3, 1, F_Real by ANPROJ_8: 4;

        reconsider z = 0 as Element of F_Real ;

        reconsider d as Element of F_Real by XREAL_0:def 1;

        

         A13: p = (N * Mu) by A5, LAPLACE:def 9

        .= <* <*(((a * d) + (z * z)) + (z * z))*>, <*(((z * d) + (b * z)) + (z * z))*>, <*(((z * d) + (z * z)) + (c * z))*>*> by A1, A12, Th08

        .= <* <*(a * d)*>, <* 0 *>, <* 0 *>*>;

        v = |[(a * d), 0 , 0 ]|

        proof

          

           A14: ( <*(a * d)*> . 1) = (a * d) & ( <* 0 *> . 1) = 0 by FINSEQ_1:def 8;

          

           A15: (p . 1) = <*(a * d)*> & (p . 2) = <* 0 *> & (p . 3) = <* 0 *> by A13, FINSEQ_1: 45;

          ( len p) = 3 by A13, FINSEQ_1: 45;

          hence thesis by A14, A15, A6, ANPROJ_8:def 2;

        end;

        

        then

         A16: v = |[(a * d), (a * 0 ), (a * 0 )]|

        .= (a * u) by A10, EUCLID_5: 8;

        a is non zero;

        then are_Prop (v,u) by A16, ANPROJ_1: 1;

        hence thesis by A2, A3, A7, A8, ANPROJ_1: 22;

      end;

      thus (( homography N) . Dir010 ) = Dir010

      proof

        consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be FinSequence of (1 -tuples_on REAL ) such that

         A17: Dir010 = ( Dir u) and

         A18: not u is zero and

         A19: u = uf and

         A20: p = (N * uf) and

         A21: v = ( M2F p) and

         A22: not v is zero and

         A23: (( homography N) . Dir010 ) = ( Dir v) by ANPROJ_8:def 4;

         not |[ 0 , 1, 0 ]| is zero by EUCLID_8:def 2, Th13;

        then are_Prop (u, |[ 0 , 1, 0 ]|) by A17, A18, ANPROJ_1: 22;

        then

        consider d be Real such that d <> 0 and

         A24: u = (d * |[ 0 , 1, 0 ]|) by ANPROJ_1: 1;

        

         A25: u = |[(d * 0 ), (d * 1), (d * 0 )]| by A24, EUCLID_5: 8

        .= |[ 0 , d, 0 ]|;

        then (u `1 ) = 0 & (u `2 ) = d & (u `3 ) = 0 by EUCLID_5: 2;

        then

         A26: (uf . 1) = 0 & (uf . 2) = d & (uf . 3) = 0 by A19, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

        u in ( TOP-REAL 3);

        then u in ( REAL 3) by EUCLID: 22;

        then

         A27: ( <*uf*> @ ) = <* <* 0 *>, <*d*>, <* 0 *>*> by A26, A19, EUCLID_8: 50, ANPROJ_8: 77;

        reconsider Mu = ( <*uf*> @ ) as Matrix of 3, 1, F_Real by A27, ANPROJ_8: 4;

        reconsider z = 0 as Element of F_Real ;

        reconsider d as Element of F_Real by XREAL_0:def 1;

        

         A28: p = (N * Mu) by A20, LAPLACE:def 9

        .= <* <*(((a * z) + (z * d)) + (z * z))*>, <*(((z * z) + (b * d)) + (z * z))*>, <*(((z * d) + (z * z)) + (c * z))*>*> by A1, A27, Th08

        .= <* <* 0 *>, <*(b * d)*>, <* 0 *>*>;

        v = |[ 0 , (b * d), 0 ]|

        proof

          

           A29: ( <* 0 *> . 1) = 0 & ( <*(b * d)*> . 1) = (b * d) by FINSEQ_1:def 8;

          

           A30: (p . 1) = <* 0 *> & (p . 2) = <*(b * d)*> & (p . 3) = <* 0 *> by A28, FINSEQ_1: 45;

          ( len p) = 3 by A28, FINSEQ_1: 45;

          hence thesis by A29, A30, A21, ANPROJ_8:def 2;

        end;

        

        then

         A31: v = |[(b * 0 ), (b * d), (b * 0 )]|

        .= (b * u) by A25, EUCLID_5: 8;

        b is non zero;

        then are_Prop (v,u) by A31, ANPROJ_1: 1;

        hence thesis by A17, A18, A22, A23, ANPROJ_1: 22;

      end;

      thus (( homography N) . Dir001 ) = Dir001

      proof

        consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be FinSequence of (1 -tuples_on REAL ) such that

         A31BIS: Dir001 = ( Dir u) and

         A32: not u is zero and

         A33: u = uf and

         A34: p = (N * uf) and

         A35: v = ( M2F p) and

         A36: not v is zero and

         A37: (( homography N) . Dir001 ) = ( Dir v) by ANPROJ_8:def 4;

         not |[ 0 , 0 , 1]| is zero by EUCLID_8:def 3, Th13;

        then are_Prop (u, |[ 0 , 0 , 1]|) by A31BIS, A32, ANPROJ_1: 22;

        then

        consider d be Real such that d <> 0 and

         A38: u = (d * |[ 0 , 0 , 1]|) by ANPROJ_1: 1;

        

         A39: u = |[(d * 0 ), (d * 0 ), (d * 1)]| by A38, EUCLID_5: 8

        .= |[ 0 , 0 , d]|;

        then (u `1 ) = 0 & (u `2 ) = 0 & (u `3 ) = d by EUCLID_5: 2;

        then

         A40: (uf . 1) = 0 & (uf . 2) = 0 & (uf . 3) = d by A33, EUCLID_5:def 1, EUCLID_5:def 2, EUCLID_5:def 3;

        u in ( TOP-REAL 3);

        then u in ( REAL 3) by EUCLID: 22;

        then

         A41: ( <*uf*> @ ) = <* <* 0 *>, <* 0 *>, <*d*>*> by A40, A33, EUCLID_8: 50, ANPROJ_8: 77;

        reconsider Mu = ( <*uf*> @ ) as Matrix of 3, 1, F_Real by A41, ANPROJ_8: 4;

        reconsider z = 0 as Element of F_Real ;

        reconsider d as Element of F_Real by XREAL_0:def 1;

        

         A42: p = (N * Mu) by A34, LAPLACE:def 9

        .= <* <*(((a * z) + (z * z)) + (z * d))*>, <*(((z * z) + (b * z)) + (z * d))*>, <*(((z * z) + (z * z)) + (c * d))*>*> by A1, A41, Th08

        .= <* <* 0 *>, <* 0 *>, <*(c * d)*>*>;

        v = |[ 0 , 0 , (c * d)]|

        proof

          

           A43: ( <*(c * d)*> . 1) = (c * d) & ( <* 0 *> . 1) = 0 by FINSEQ_1:def 8;

          

           A44: (p . 3) = <*(c * d)*> & (p . 2) = <* 0 *> & (p . 1) = <* 0 *> by A42, FINSEQ_1: 45;

          ( len p) = 3 by A42, FINSEQ_1: 45;

          hence thesis by A43, A44, A35, ANPROJ_8:def 2;

        end;

        

        then

         A45: v = |[(c * 0 ), (c * 0 ), (c * d)]|

        .= (c * u) by A39, EUCLID_5: 8;

        c is non zero;

        then are_Prop (v,u) by A45, ANPROJ_1: 1;

        hence thesis by A31BIS, A32, A36, A37, ANPROJ_1: 22;

      end;

    end;

    theorem :: ANPROJ_9:26

    

     Th22: for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) holds ex a,b,c be Element of F_Real st P = ( Dir |[a, b, c]|) & (a <> 0 or b <> 0 or c <> 0 )

    proof

      let P be Point of ( ProjectiveSpace ( TOP-REAL 3));

      consider u be Element of ( TOP-REAL 3) such that

       A1: u is non zero and

       A2: P = ( Dir u) by ANPROJ_1: 26;

      

       A3: u = |[(u `1 ), (u `2 ), (u `3 )]| by EUCLID_5: 3

      .= |[(u . 1), (u `2 ), (u `3 )]| by EUCLID_5:def 1

      .= |[(u . 1), (u . 2), (u `3 )]| by EUCLID_5:def 2

      .= |[(u . 1), (u . 2), (u . 3)]| by EUCLID_5:def 3;

      reconsider a = (u . 1), b = (u . 2), c = (u . 3) as Element of F_Real by XREAL_0:def 1;

      take a, b, c;

      thus P = ( Dir |[a, b, c]|) by A2, A3;

      thus a <> 0 or b <> 0 or c <> 0 by A1, A3, EUCLID_5: 4;

    end;

    

     Lem07: for a,b,c be Element of F_Real holds for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) st P = ( Dir |[a, b, c]|) & (a <> 0 or b <> 0 or c <> 0 ) holds ( not (( Dir100 , Dir010 ,P) are_collinear ) implies c <> 0 ) & ( not (( Dir100 , Dir001 ,P) are_collinear ) implies b <> 0 ) & ( not (( Dir010 , Dir001 ,P) are_collinear ) implies a <> 0 )

    proof

      let a,b,c be Element of F_Real ;

      let P be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: P = ( Dir |[a, b, c]|) and

       A2: a <> 0 or b <> 0 or c <> 0 ;

      thus not (( Dir100 , Dir010 ,P) are_collinear ) implies c <> 0

      proof

        assume

         A3: not ( Dir100 , Dir010 ,P) are_collinear ;

        assume

         A4: c = 0 ;

        

         A5: not |[a, b, c]| is zero by A2, EUCLID_5: 4, FINSEQ_1: 78;

        

         A6: not ( |[1, 0 , 0 ]|, |[ 0 , 1, 0 ]|, |[a, b, c]|) are_LinDep by A3, ANPROJ_2: 23, Th11, A5, A1;

        (((( - a) * |[1, 0 , 0 ]|) + (( - b) * |[ 0 , 1, 0 ]|)) + (1 * |[a, b, c]|)) = (( |[(( - a) * 1), (( - a) * 0 ), (( - a) * 0 )]| + (( - b) * |[ 0 , 1, 0 ]|)) + (1 * |[a, b, c]|)) by EUCLID_5: 8

        .= (( |[( - a), 0 , 0 ]| + |[(( - b) * 0 ), (( - b) * 1), (( - b) * 0 )]|) + (1 * |[a, b, c]|)) by EUCLID_5: 8

        .= (( |[( - a), 0 , 0 ]| + |[ 0 , ( - b), 0 ]|) + |[(1 * a), (1 * b), (1 * c)]|) by EUCLID_5: 8

        .= ( |[(( - a) + 0 ), ( 0 + ( - b)), ( 0 + 0 )]| + |[a, b, c]|) by EUCLID_5: 6

        .= |[(( - a) + a), (( - b) + b), ( 0 + c)]| by EUCLID_5: 6

        .= ( 0. ( TOP-REAL 3)) by A4, EUCLID_5: 4;

        hence contradiction by A6, ANPROJ_1:def 2;

      end;

      thus not (( Dir100 , Dir001 ,P) are_collinear ) implies b <> 0

      proof

        assume

         A7: not ( Dir100 , Dir001 ,P) are_collinear ;

        assume

         A8: b = 0 ;

        

         A9: not |[a, b, c]| is zero by A2, EUCLID_5: 4, FINSEQ_1: 78;

        

         A10: not ( |[1, 0 , 0 ]|, |[ 0 , 0 , 1]|, |[a, b, c]|) are_LinDep by A7, ANPROJ_2: 23, Th11, A9, A1;

        (((( - a) * |[1, 0 , 0 ]|) + (( - c) * |[ 0 , 0 , 1]|)) + (1 * |[a, b, c]|)) = (( |[(( - a) * 1), (( - a) * 0 ), (( - a) * 0 )]| + (( - c) * |[ 0 , 0 , 1]|)) + (1 * |[a, b, c]|)) by EUCLID_5: 8

        .= (( |[( - a), 0 , 0 ]| + |[(( - c) * 0 ), (( - c) * 0 ), (( - c) * 1)]|) + (1 * |[a, b, c]|)) by EUCLID_5: 8

        .= (( |[( - a), 0 , 0 ]| + |[ 0 , 0 , ( - c)]|) + |[(1 * a), (1 * b), (1 * c)]|) by EUCLID_5: 8

        .= ( |[(( - a) + 0 ), ( 0 + 0 ), ( 0 + ( - c))]| + |[a, b, c]|) by EUCLID_5: 6

        .= |[(( - a) + a), ( 0 + b), (( - c) + c)]| by EUCLID_5: 6

        .= ( 0. ( TOP-REAL 3)) by A8, EUCLID_5: 4;

        hence contradiction by A10, ANPROJ_1:def 2;

      end;

      thus not (( Dir010 , Dir001 ,P) are_collinear ) implies a <> 0

      proof

        assume

         A11: not ( Dir010 , Dir001 ,P) are_collinear ;

        assume

         A12: a = 0 ;

        

         A13: not |[a, b, c]| is zero by A2, EUCLID_5: 4, FINSEQ_1: 78;

        

         A14: not ( |[ 0 , 1, 0 ]|, |[ 0 , 0 , 1]|, |[a, b, c]|) are_LinDep by A11, ANPROJ_2: 23, Th11, A13, A1;

        (((( - b) * |[ 0 , 1, 0 ]|) + (( - c) * |[ 0 , 0 , 1]|)) + (1 * |[a, b, c]|)) = (( |[(( - b) * 0 ), (( - b) * 1), (( - b) * 0 )]| + (( - c) * |[ 0 , 0 , 1]|)) + (1 * |[a, b, c]|)) by EUCLID_5: 8

        .= (( |[ 0 , ( - b), 0 ]| + |[(( - c) * 0 ), (( - c) * 0 ), (( - c) * 1)]|) + (1 * |[a, b, c]|)) by EUCLID_5: 8

        .= (( |[ 0 , ( - b), 0 ]| + |[ 0 , 0 , ( - c)]|) + |[(1 * a), (1 * b), (1 * c)]|) by EUCLID_5: 8

        .= ( |[( 0 + 0 ), (( - b) + 0 ), ( 0 + ( - c))]| + |[a, b, c]|) by EUCLID_5: 6

        .= |[( 0 + a), (( - b) + b), (( - c) + c)]| by EUCLID_5: 6

        .= ( 0. ( TOP-REAL 3)) by A12, EUCLID_5: 4;

        hence contradiction by A14, ANPROJ_1:def 2;

      end;

    end;

    theorem :: ANPROJ_9:27

    

     Th23: for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) st not (( Dir100 , Dir010 ,P) are_collinear ) & not (( Dir100 , Dir001 ,P) are_collinear ) & not (( Dir010 , Dir001 ,P) are_collinear ) holds ex a,b,c be non zero Element of F_Real st P = ( Dir |[a, b, c]|)

    proof

      let P be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: not (( Dir100 , Dir010 ,P) are_collinear ) and

       A2: not (( Dir100 , Dir001 ,P) are_collinear ) and

       A3: not (( Dir010 , Dir001 ,P) are_collinear );

      consider a,b,c be Element of F_Real such that

       A4: P = ( Dir |[a, b, c]|) and

       A5: (a <> 0 or b <> 0 or c <> 0 ) by Th22;

      a is non zero & b is non zero & c is non zero by A1, A2, A3, A4, A5, Lem07;

      then

      reconsider a, b, c as non zero Element of F_Real ;

      take a, b, c;

      thus thesis by A4;

    end;

    theorem :: ANPROJ_9:28

    

     Th24: for a,b,c,ia,ib,ic be non zero Element of F_Real holds for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) holds for N be 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]|)

    proof

      let a,b,c,ia,ib,ic be non zero Element of F_Real ;

      let P be Point of ( ProjectiveSpace ( TOP-REAL 3));

      let N be invertible Matrix of 3, F_Real ;

      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*>*>;

      consider u,v be Element of ( TOP-REAL 3), uf be FinSequence of F_Real , p be 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;

       |[a, b, c]| is non zero

      proof

        assume |[a, b, c]| is zero;

        then a is zero & b is zero & c is zero by EUCLID_5: 4, FINSEQ_1: 78;

        hence thesis;

      end;

      then are_Prop (u, |[a, b, c]|) by A1, A15, A16, ANPROJ_1: 22;

      then

      consider d be 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, FINSEQ_1: 45;

      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) by FINSEQ_1:def 8;

        

         A30: (p . 1) = <*(ia * da)*> & (p . 2) = <*(ib * db)*> & (p . 3) = <*(ic * dc)*> by A27, FINSEQ_1: 45;

        ( len p) = 3 by A27, FINSEQ_1: 45;

        hence thesis by A29, A30, A19, ANPROJ_8:def 2;

      end;

      

       A31: a is non zero & b is non zero & c is non zero;

      now

        

        thus (ia * da) = (((1 / a) * a) * d) by A2

        .= (1 * d) by A31, XCMPLX_1: 106

        .= d;

        

        thus (ib * db) = (((1 / b) * b) * d) by A3

        .= (1 * d) by A31, XCMPLX_1: 106

        .= d;

        

        thus (ic * dc) = (((1 / c) * c) * d) by A4

        .= (1 * d) by A31, XCMPLX_1: 106

        .= d;

      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 thesis by Th11, A20, ANPROJ_1: 22, A21;

    end;

    theorem :: ANPROJ_9:29

    

     Th25: for P be Point of ( ProjectiveSpace ( TOP-REAL 3)) st not (( Dir100 , Dir010 ,P) are_collinear ) & not (( Dir100 , Dir001 ,P) are_collinear ) & not (( Dir010 , Dir001 ,P) are_collinear ) holds ex a,b,c be non zero Element of F_Real st for N be invertible Matrix of 3, F_Real st N = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> holds (( homography N) . P) = Dir111

    proof

      let P be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: not (( Dir100 , Dir010 ,P) are_collinear ) and

       A2: not (( Dir100 , Dir001 ,P) are_collinear ) and

       A3: not (( Dir010 , Dir001 ,P) are_collinear );

      consider a,b,c be non zero Element of F_Real such that

       A4: P = ( Dir |[a, b, c]|) by Th23, A1, A2, A3;

      reconsider ia = (1 / a), ib = (1 / b), ic = (1 / c) as Element of F_Real by XREAL_0:def 1;

      ia is non zero & ib is non zero & ic is non zero by XCMPLX_1: 50;

      then

      reconsider ia, ib, ic as non zero Element of F_Real ;

      take ia, ib, ic;

      thus thesis by A4, Th24;

    end;

    theorem :: ANPROJ_9:30

    

     Th26: for P1,P2,P3,P4 be Point of ( ProjectiveSpace ( TOP-REAL 3)) st not ((P1,P2,P3) are_collinear ) & not ((P1,P2,P4) are_collinear ) & not ((P1,P3,P4) are_collinear ) & not ((P2,P3,P4) are_collinear ) holds ex N be invertible Matrix of 3, F_Real st (( homography N) . P1) = Dir100 & (( homography N) . P2) = Dir010 & (( homography N) . P3) = Dir001 & (( homography N) . P4) = Dir111

    proof

      let P1,P2,P3,P4 be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: not ((P1,P2,P3) are_collinear ) and

       A2: not ((P1,P2,P4) are_collinear ) and

       A3: not ((P1,P3,P4) are_collinear ) and

       A4: not ((P2,P3,P4) are_collinear );

      consider N1 be invertible Matrix of 3, F_Real such that

       A5: (( homography N1) . P1) = Dir100 and

       A6: (( homography N1) . P2) = Dir010 and

       A7: (( homography N1) . P3) = Dir001 by A1, Th20;

      set Q1 = (( homography N1) . P1), Q2 = (( homography N1) . P2), Q3 = (( homography N1) . P3), Q4 = (( homography N1) . P4);

       not ((Q1,Q2,Q3) are_collinear ) & not ((Q1,Q2,Q4) are_collinear ) & not ((Q1,Q3,Q4) are_collinear ) & not ((Q2,Q3,Q4) are_collinear ) by A1, A2, A3, A4, ANPROJ_8: 102;

      then

      consider a,b,c be non zero Element of F_Real such that

       A8: for N2 be invertible Matrix of 3, F_Real st N2 = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> holds (( homography N2) . Q4) = Dir111 by A5, A6, A7, Th25;

      reconsider N2 = <* <*a, 0 , 0 *>, <* 0 , b, 0 *>, <* 0 , 0 , c*>*> as invertible Matrix of 3, F_Real by Th10;

      reconsider N = (N2 * N1) as invertible Matrix of 3, F_Real ;

      take N;

      now

        

        thus Dir100 = (( homography N2) . Q1) by A5, Th21

        .= (( homography (N2 * N1)) . P1) by Th14;

        

        thus Dir010 = (( homography N2) . Q2) by A6, Th21

        .= (( homography (N2 * N1)) . P2) by Th14;

        

        thus Dir001 = (( homography N2) . Q3) by A7, Th21

        .= (( homography (N2 * N1)) . P3) by Th14;

        

        thus Dir111 = (( homography N2) . Q4) by A8

        .= (( homography (N2 * N1)) . P4) by Th14;

      end;

      hence thesis;

    end;

    theorem :: ANPROJ_9:31

    for P1,P2,P3,P4,Q1,Q2,Q3,Q4 be Point of ( ProjectiveSpace ( TOP-REAL 3)) st not ((P1,P2,P3) are_collinear ) & not ((P1,P2,P4) are_collinear ) & not ((P1,P3,P4) are_collinear ) & not ((P2,P3,P4) are_collinear ) & not ((Q1,Q2,Q3) are_collinear ) & not ((Q1,Q2,Q4) are_collinear ) & not ((Q1,Q3,Q4) are_collinear ) & not ((Q2,Q3,Q4) are_collinear ) holds ex N be invertible Matrix of 3, F_Real st (( homography N) . P1) = Q1 & (( homography N) . P2) = Q2 & (( homography N) . P3) = Q3 & (( homography N) . P4) = Q4

    proof

      let P1,P2,P3,P4,Q1,Q2,Q3,Q4 be Point of ( ProjectiveSpace ( TOP-REAL 3));

      assume that

       A1: not ((P1,P2,P3) are_collinear ) & not ((P1,P2,P4) are_collinear ) & not ((P1,P3,P4) are_collinear ) & not ((P2,P3,P4) are_collinear ) and

       A2: not ((Q1,Q2,Q3) are_collinear ) & not ((Q1,Q2,Q4) are_collinear ) & not ((Q1,Q3,Q4) are_collinear ) & not ((Q2,Q3,Q4) are_collinear );

      consider N1 be invertible Matrix of 3, F_Real such that

       A3: (( homography N1) . P1) = Dir100 & (( homography N1) . P2) = Dir010 & (( homography N1) . P3) = Dir001 & (( homography N1) . P4) = Dir111 by A1, Th26;

      consider N2 be invertible Matrix of 3, F_Real such that

       A4: (( homography N2) . Q1) = Dir100 & (( homography N2) . Q2) = Dir010 & (( homography N2) . Q3) = Dir001 & (( homography N2) . Q4) = Dir111 by A2, Th26;

      reconsider N = ((N2 ~ ) * N1) as invertible Matrix of 3, F_Real ;

      take N;

      

      thus Q1 = (( homography (N2 ~ )) . (( homography N1) . P1)) by A3, A4, Th16

      .= (( homography N) . P1) by Th14;

      

      thus Q2 = (( homography (N2 ~ )) . (( homography N1) . P2)) by A3, A4, Th16

      .= (( homography N) . P2) by Th14;

      

      thus Q3 = (( homography (N2 ~ )) . (( homography N1) . P3)) by A3, A4, Th16

      .= (( homography N) . P3) by Th14;

      

      thus Q4 = (( homography (N2 ~ )) . (( homography N1) . P4)) by A3, A4, Th16

      .= (( homography N) . P4) by Th14;

    end;