goboard1.miz



    begin

    reserve p for Point of ( TOP-REAL 2),

f,f1,f2,g for FinSequence of ( TOP-REAL 2),

v,v1,v2 for FinSequence of REAL ,

r,s for Real,

n,m,i,j,k for Nat,

x for set;

    definition

      let f;

      :: GOBOARD1:def1

      func X_axis (f) -> FinSequence of REAL means

      : Def1: ( len it ) = ( len f) & for n st n in ( dom it ) holds (it . n) = ((f /. n) `1 );

      existence

      proof

        defpred P[ Nat, set] means $2 = ((f /. $1) `1 );

        

         A1: for k be Nat st k in ( Seg ( len f)) holds ex r be Element of REAL st P[k, r]

        proof

          let k be Nat;

          ((f /. k) `1 ) in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider v such that

         A2: ( dom v) = ( Seg ( len f)) and

         A3: for k be Nat st k in ( Seg ( len f)) holds P[k, (v . k)] from FINSEQ_1:sch 5( A1);

        take v;

        thus ( len v) = ( len f) by A2, FINSEQ_1:def 3;

        let n;

        assume n in ( dom v);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

        let v1, v2;

        assume that

         A4: ( len v1) = ( len f) and

         A5: for n st n in ( dom v1) holds (v1 . n) = ((f /. n) `1 ) and

         A6: ( len v2) = ( len f) and

         A7: for n st n in ( dom v2) holds (v2 . n) = ((f /. n) `1 );

        

         A8: ( dom v2) = ( Seg ( len v2)) by FINSEQ_1:def 3;

        

         A9: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        

         A10: ( dom v1) = ( Seg ( len v1)) by FINSEQ_1:def 3;

        now

          let n be Nat;

          assume

           A11: n in ( dom f);

          

          hence (v1 . n) = ((f /. n) `1 ) by A4, A5, A10, A9

          .= (v2 . n) by A6, A7, A8, A9, A11;

        end;

        hence thesis by A4, A6, A10, A8, A9, FINSEQ_1: 13;

      end;

      :: GOBOARD1:def2

      func Y_axis (f) -> FinSequence of REAL means

      : Def2: ( len it ) = ( len f) & for n st n in ( dom it ) holds (it . n) = ((f /. n) `2 );

      existence

      proof

        defpred P[ Nat, set] means $2 = ((f /. $1) `2 );

        

         A12: for k be Nat st k in ( Seg ( len f)) holds ex r be Element of REAL st P[k, r]

        proof

          let k be Nat;

          ((f /. k) `2 ) in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider v such that

         A13: ( dom v) = ( Seg ( len f)) and

         A14: for k be Nat st k in ( Seg ( len f)) holds P[k, (v . k)] from FINSEQ_1:sch 5( A12);

        take v;

        thus ( len v) = ( len f) by A13, FINSEQ_1:def 3;

        let n;

        assume n in ( dom v);

        hence thesis by A13, A14;

      end;

      uniqueness

      proof

        let v1, v2;

        assume that

         A15: ( len v1) = ( len f) and

         A16: for n st n in ( dom v1) holds (v1 . n) = ((f /. n) `2 ) and

         A17: ( len v2) = ( len f) and

         A18: for n st n in ( dom v2) holds (v2 . n) = ((f /. n) `2 );

        

         A19: ( dom v2) = ( Seg ( len v2)) by FINSEQ_1:def 3;

        

         A20: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

        

         A21: ( dom v1) = ( Seg ( len v1)) by FINSEQ_1:def 3;

        now

          let n be Nat;

          assume

           A22: n in ( dom f);

          

          hence (v1 . n) = ((f /. n) `2 ) by A15, A16, A21, A20

          .= (v2 . n) by A17, A18, A19, A20, A22;

        end;

        hence thesis by A15, A17, A21, A19, A20, FINSEQ_1: 13;

      end;

    end

    theorem :: GOBOARD1:1

    

     Th1: i in ( dom f) & 2 <= ( len f) implies (f /. i) in ( L~ f)

    proof

      assume that

       A1: i in ( dom f) and

       A2: 2 <= ( len f);

      

       A3: 1 <= i by A1, FINSEQ_3: 25;

      

       A4: i <= ( len f) by A1, FINSEQ_3: 25;

      per cases by A4, XXREAL_0: 1;

        suppose

         A5: i = ( len f);

        reconsider l = (i - 1) as Element of NAT by A3, INT_1: 5;

        (1 + 1) <= i by A2, A5;

        then 1 <= l by XREAL_1: 19;

        then

         A6: (f /. (l + 1)) in ( LSeg (f,l)) by A4, TOPREAL1: 21;

        ( LSeg (f,l)) c= ( L~ f) by TOPREAL3: 19;

        hence thesis by A6;

      end;

        suppose i < ( len f);

        then (i + 1) <= ( len f) by NAT_1: 13;

        then

         A7: (f /. i) in ( LSeg (f,i)) by A3, TOPREAL1: 21;

        ( LSeg (f,i)) c= ( L~ f) by TOPREAL3: 19;

        hence thesis by A7;

      end;

    end;

    begin

    definition

      ::$Canceled

      let M be Matrix of ( TOP-REAL 2);

      :: GOBOARD1:def4

      attr M is X_equal-in-line means

      : Def3: for n st n in ( dom M) holds ( X_axis ( Line (M,n))) is constant;

      :: GOBOARD1:def5

      attr M is Y_equal-in-column means

      : Def4: for n st n in ( Seg ( width M)) holds ( Y_axis ( Col (M,n))) is constant;

      :: GOBOARD1:def6

      attr M is Y_increasing-in-line means

      : Def5: for n st n in ( dom M) holds ( Y_axis ( Line (M,n))) is increasing;

      :: GOBOARD1:def7

      attr M is X_increasing-in-column means

      : Def6: for n st n in ( Seg ( width M)) holds ( X_axis ( Col (M,n))) is increasing;

    end

    registration

      cluster non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column for Matrix of ( TOP-REAL 2);

      existence

      proof

        set p = the Point of ( TOP-REAL 2);

        take M = <* <*p*>*>;

        

         A1: ( len M) = 1 by MATRIX_0: 24;

        

         A2: ( width M) = 1 by MATRIX_0: 24;

        hence M is non empty-yielding by A1, MATRIX_0:def 10;

        thus M is X_equal-in-line

        proof

          let n such that n in ( dom M);

          set L = ( X_axis ( Line (M,n)));

          let k;

          let m be Nat;

          assume that

           A3: k in ( dom L) and

           A4: m in ( dom L);

          

           A5: ( len L) = ( len ( Line (M,n))) by Def1;

          k in ( Seg ( len L)) by A3, FINSEQ_1:def 3;

          then k in {1} by A2, A5, FINSEQ_1: 2, MATRIX_0:def 7;

          then

           A6: k = 1 by TARSKI:def 1;

          m in ( Seg ( len L)) by A4, FINSEQ_1:def 3;

          then m in {1} by A2, A5, FINSEQ_1: 2, MATRIX_0:def 7;

          hence (L . k) = (L . m) by A6, TARSKI:def 1;

        end;

        thus M is Y_equal-in-column

        proof

          let n such that n in ( Seg ( width M));

          set L = ( Y_axis ( Col (M,n)));

          let k, m;

          assume that

           A7: k in ( dom L) and

           A8: m in ( dom L);

          

           A9: ( len L) = ( len ( Col (M,n))) by Def2;

          k in ( Seg ( len L)) by A7, FINSEQ_1:def 3;

          then k in {1} by A1, A9, FINSEQ_1: 2, MATRIX_0:def 8;

          then

           A10: k = 1 by TARSKI:def 1;

          m in ( Seg ( len L)) by A8, FINSEQ_1:def 3;

          then m in {1} by A1, A9, FINSEQ_1: 2, MATRIX_0:def 8;

          hence (L . k) = (L . m) by A10, TARSKI:def 1;

        end;

        thus M is Y_increasing-in-line

        proof

          let n such that n in ( dom M);

          set L = ( Y_axis ( Line (M,n)));

          let k, m;

          assume that

           A11: k in ( dom L) and

           A12: m in ( dom L) and

           A13: k < m;

          

           A14: ( len L) = ( len ( Line (M,n))) by Def2;

          k in ( Seg ( len L)) by A11, FINSEQ_1:def 3;

          then k in {1} by A2, A14, FINSEQ_1: 2, MATRIX_0:def 7;

          then

           A15: k = 1 by TARSKI:def 1;

          m in ( Seg ( len L)) by A12, FINSEQ_1:def 3;

          then m in {1} by A2, A14, FINSEQ_1: 2, MATRIX_0:def 7;

          hence thesis by A13, A15, TARSKI:def 1;

        end;

        let n such that n in ( Seg ( width M));

        set L = ( X_axis ( Col (M,n)));

        let k, m;

        assume that

         A16: k in ( dom L) and

         A17: m in ( dom L) and

         A18: k < m;

        

         A19: ( len L) = ( len ( Col (M,n))) by Def1;

        k in ( Seg ( len L)) by A16, FINSEQ_1:def 3;

        then k in {1} by A1, A19, FINSEQ_1: 2, MATRIX_0:def 8;

        then

         A20: k = 1 by TARSKI:def 1;

        m in ( Seg ( len L)) by A17, FINSEQ_1:def 3;

        then m in {1} by A1, A19, FINSEQ_1: 2, MATRIX_0:def 8;

        hence thesis by A18, A20, TARSKI:def 1;

      end;

    end

    ::$Canceled

    theorem :: GOBOARD1:3

    

     Th2: for M be X_increasing-in-column X_equal-in-line Matrix of ( TOP-REAL 2) holds for x, n, m st x in ( rng ( Line (M,n))) & x in ( rng ( Line (M,m))) & n in ( dom M) & m in ( dom M) holds n = m

    proof

      let M be X_increasing-in-column X_equal-in-line Matrix of ( TOP-REAL 2);

      assume not thesis;

      then

      consider x, n, m such that

       A1: x in ( rng ( Line (M,n))) and

       A2: x in ( rng ( Line (M,m))) and

       A3: n in ( dom M) and

       A4: m in ( dom M) and

       A5: n <> m;

      

       A6: n < m or m < n by A5, XXREAL_0: 1;

      

       A7: ( X_axis ( Line (M,m))) is constant by A4, Def3;

      reconsider Ln = ( Line (M,n)), Lm = ( Line (M,m)) as FinSequence of ( TOP-REAL 2);

      consider i be Nat such that

       A8: i in ( dom Ln) and

       A9: (Ln . i) = x by A1, FINSEQ_2: 10;

      set C = ( X_axis ( Col (M,i)));

      

       A10: ( len Ln) = ( width M) by MATRIX_0:def 7;

      reconsider Mi = ( Col (M,i)) as FinSequence of ( TOP-REAL 2);

      

       A11: (( Col (M,i)) . n) = (M * (n,i)) by A3, MATRIX_0:def 8;

      

       A12: ( len ( Col (M,i))) = ( len M) by MATRIX_0:def 8;

      then n in ( dom ( Col (M,i))) by A3, FINSEQ_3: 29;

      then

       A13: (M * (n,i)) = (Mi /. n) by A11, PARTFUN1:def 6;

      

       A14: (( Col (M,i)) . m) = (M * (m,i)) by A4, MATRIX_0:def 8;

      

       A15: ( dom M) = ( Seg ( len M)) by FINSEQ_1:def 3;

      then m in ( dom ( Col (M,i))) by A4, A12, FINSEQ_1:def 3;

      then

       A16: (M * (m,i)) = (Mi /. m) by A14, PARTFUN1:def 6;

      consider j be Nat such that

       A17: j in ( dom Lm) and

       A18: (Lm . j) = x by A2, FINSEQ_2: 10;

      

       A19: ( len C) = ( len ( Col (M,i))) & ( dom C) = ( Seg ( len C)) by Def1, FINSEQ_1:def 3;

      

       A20: ( Seg ( len Ln)) = ( dom Ln) by FINSEQ_1:def 3;

      then

       A21: C is increasing by A8, A10, Def6;

      

       A22: ( len Lm) = ( width M) by MATRIX_0:def 7;

      then

       A23: i in ( dom Lm) by A8, A10, FINSEQ_3: 29;

      (Lm . i) = (M * (m,i)) by A8, A10, A20, MATRIX_0:def 7;

      then

       A24: (Lm /. i) = (M * (m,i)) by A23, PARTFUN1:def 6;

      

       A25: ( dom ( X_axis Lm)) = ( Seg ( len ( X_axis Lm))) by FINSEQ_1:def 3;

      (Ln . i) = (M * (n,i)) by A8, A10, A20, MATRIX_0:def 7;

      then

      reconsider p = x as Point of ( TOP-REAL 2) by A9;

      

       A26: (Lm /. j) = p by A17, A18, PARTFUN1:def 6;

      

       A27: ( len ( X_axis Lm)) = ( len Lm) by Def1;

      then

       A28: j in ( dom ( X_axis Lm)) by A17, FINSEQ_3: 29;

      ( Seg ( len Lm)) = ( dom Lm) by FINSEQ_1:def 3;

      then

       A29: j in ( dom ( X_axis Lm)) by A17, A25, Def1;

      i in ( dom ( X_axis Lm)) by A8, A10, A22, A27, FINSEQ_3: 29;

      then (( X_axis Lm) . i) = (( X_axis Lm) . j) by A7, A28;

      

      then

       A30: ((M * (m,i)) `1 ) = (( X_axis Lm) . j) by A8, A25, A10, A22, A27, A20, A24, Def1

      .= (p `1 ) by A29, A26, Def1;

      ((M * (n,i)) `1 ) = (p `1 ) by A8, A9, A10, A20, MATRIX_0:def 7;

      

      then (C . n) = (p `1 ) by A3, A15, A12, A19, A13, Def1

      .= (C . m) by A4, A15, A12, A19, A30, A16, Def1;

      hence contradiction by A3, A4, A15, A21, A12, A19, A6;

    end;

    theorem :: GOBOARD1:4

    

     Th3: for M be Y_increasing-in-line Y_equal-in-column Matrix of ( TOP-REAL 2) holds for x, n, m st x in ( rng ( Col (M,n))) & x in ( rng ( Col (M,m))) & n in ( Seg ( width M)) & m in ( Seg ( width M)) holds n = m

    proof

      let M be Y_increasing-in-line Y_equal-in-column Matrix of ( TOP-REAL 2);

      assume not thesis;

      then

      consider x, n, m such that

       A1: x in ( rng ( Col (M,n))) and

       A2: x in ( rng ( Col (M,m))) and

       A3: n in ( Seg ( width M)) and

       A4: m in ( Seg ( width M)) and

       A5: n <> m;

      reconsider Ln = ( Col (M,n)), Lm = ( Col (M,m)) as FinSequence of ( TOP-REAL 2);

      consider i be Nat such that

       A6: i in ( dom Ln) and

       A7: (Ln . i) = x by A1, FINSEQ_2: 10;

      

       A8: ( len Ln) = ( len M) by MATRIX_0:def 8;

      

       A9: ( len Lm) = ( len M) by MATRIX_0:def 8;

      then

       A10: i in ( dom Lm) by A6, A8, FINSEQ_3: 29;

      set C = ( Y_axis ( Line (M,i)));

      

       A11: ( Seg ( len Ln)) = ( dom Ln) by FINSEQ_1:def 3;

      

       A12: ( dom M) = ( Seg ( len M)) by FINSEQ_1:def 3;

      then

       A13: C is increasing by A6, A8, A11, Def5;

      (Lm . i) = (M * (i,m)) by A6, A8, A12, A11, MATRIX_0:def 8;

      then

       A14: (Lm /. i) = (M * (i,m)) by A10, PARTFUN1:def 6;

      

       A15: ( len ( Y_axis Lm)) = ( len Lm) by Def2;

      consider j be Nat such that

       A16: j in ( dom Lm) and

       A17: (Lm . j) = x by A2, FINSEQ_2: 10;

      

       A18: ( dom ( Y_axis Lm)) = ( Seg ( len ( Y_axis Lm))) by FINSEQ_1:def 3;

      (Ln . i) = (M * (i,n)) by A6, A8, A12, A11, MATRIX_0:def 8;

      then

      reconsider p = x as Point of ( TOP-REAL 2) by A7;

      

       A19: (Lm /. j) = p by A16, A17, PARTFUN1:def 6;

      

       A20: ( Seg ( len Lm)) = ( dom Lm) by FINSEQ_1:def 3;

      then

       A21: j in ( dom ( Y_axis Lm)) by A16, A18, Def2;

      ( Y_axis ( Col (M,m))) is constant by A4, Def4;

      then (( Y_axis Lm) . i) = (( Y_axis Lm) . j) by A6, A16, A18, A8, A9, A15, A11, A20;

      

      then

       A22: ((M * (i,m)) `2 ) = (( Y_axis Lm) . j) by A6, A18, A8, A9, A15, A11, A14, Def2

      .= (p `2 ) by A21, A19, Def2;

      

       A23: n < m or m < n by A5, XXREAL_0: 1;

      

       A24: ( len C) = ( len ( Line (M,i))) & ( dom C) = ( Seg ( len C)) by Def2, FINSEQ_1:def 3;

      reconsider Li = ( Line (M,i)) as FinSequence of ( TOP-REAL 2);

      

       A25: (( Line (M,i)) . m) = (M * (i,m)) by A4, MATRIX_0:def 7;

      

       A26: ( len ( Line (M,i))) = ( width M) by MATRIX_0:def 7;

      then m in ( dom ( Line (M,i))) by A4, FINSEQ_1:def 3;

      then

       A27: (M * (i,m)) = (Li /. m) by A25, PARTFUN1:def 6;

      

       A28: (( Line (M,i)) . n) = (M * (i,n)) by A3, MATRIX_0:def 7;

      n in ( dom ( Line (M,i))) by A3, A26, FINSEQ_1:def 3;

      then

       A29: (M * (i,n)) = (Li /. n) by A28, PARTFUN1:def 6;

      ((M * (i,n)) `2 ) = (p `2 ) by A6, A7, A8, A12, A11, MATRIX_0:def 8;

      

      then (C . n) = (p `2 ) by A3, A26, A24, A29, Def2

      .= (C . m) by A4, A26, A24, A22, A27, Def2;

      hence contradiction by A3, A4, A13, A26, A24, A23;

    end;

    begin

    definition

      mode Go-board is non empty-yielding X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column Matrix of ( TOP-REAL 2);

    end

    reserve G for Go-board;

    theorem :: GOBOARD1:5

    x = (G * (m,k)) & x = (G * (i,j)) & [m, k] in ( Indices G) & [i, j] in ( Indices G) implies m = i & k = j

    proof

      assume that

       A1: x = (G * (m,k)) and

       A2: x = (G * (i,j)) and

       A3: [m, k] in ( Indices G) and

       A4: [i, j] in ( Indices G);

      

       A5: ( len ( Line (G,m))) = ( width G) & ( dom ( Line (G,m))) = ( Seg ( len ( Line (G,m)))) by FINSEQ_1:def 3, MATRIX_0:def 7;

      

       A6: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      then

       A7: k in ( Seg ( width G)) by A3, ZFMISC_1: 87;

      then x = (( Line (G,m)) . k) by A1, MATRIX_0:def 7;

      then

       A8: x in ( rng ( Line (G,m))) by A7, A5, FUNCT_1:def 3;

      

       A9: ( len ( Col (G,k))) = ( len G) & ( dom ( Col (G,k))) = ( Seg ( len ( Col (G,k)))) by FINSEQ_1:def 3, MATRIX_0:def 8;

      

       A10: ( len ( Line (G,i))) = ( width G) & ( dom ( Line (G,i))) = ( Seg ( len ( Line (G,i)))) by FINSEQ_1:def 3, MATRIX_0:def 7;

      

       A11: ( len ( Col (G,j))) = ( len G) & ( dom ( Col (G,j))) = ( Seg ( len ( Col (G,j)))) by FINSEQ_1:def 3, MATRIX_0:def 8;

      

       A12: ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      

       A13: j in ( Seg ( width G)) by A4, A6, ZFMISC_1: 87;

      then x = (( Line (G,i)) . j) by A2, MATRIX_0:def 7;

      then

       A14: x in ( rng ( Line (G,i))) by A13, A10, FUNCT_1:def 3;

      

       A15: i in ( dom G) by A4, A6, ZFMISC_1: 87;

      then x = (( Col (G,j)) . i) by A2, MATRIX_0:def 8;

      then

       A16: x in ( rng ( Col (G,j))) by A15, A12, A11, FUNCT_1:def 3;

      

       A17: m in ( dom G) by A3, A6, ZFMISC_1: 87;

      then x = (( Col (G,k)) . m) by A1, MATRIX_0:def 8;

      then x in ( rng ( Col (G,k))) by A17, A12, A9, FUNCT_1:def 3;

      hence thesis by A17, A15, A7, A13, A8, A14, A16, Th2, Th3;

    end;

    ::$Canceled

    registration

      let G;

      let i be Nat;

      cluster ( DelCol (G,i)) -> X_equal-in-line Y_equal-in-column Y_increasing-in-line X_increasing-in-column;

      coherence

      proof

        per cases ;

          suppose not i in ( Seg ( width G));

          then ( DelCol (G,i)) = G by MATRIX_0: 61;

          hence thesis;

        end;

          suppose

           A1: i in ( Seg ( width G));

           0 < ( len G) & 0 < ( width G) by MATRIX_0: 44;

          then

          consider m be Nat such that

           A2: ( width G) = (m + 1) by NAT_1: 6;

          reconsider m as Element of NAT by ORDINAL1:def 12;

          set M = ( DelCol (G,i));

          

           A3: ( width ( DelCol (G,i))) = m by A1, A2, MATRIX_0: 63;

          then

           A4: ( len M) = ( len G) & ( width M) = m by MATRIX_0:def 13;

          then

           A5: ( dom G) = ( dom M) by FINSEQ_3: 29;

          then

           A6: ( Indices M) = [:( dom G), ( Seg m):] by A4, MATRIX_0:def 4;

          

           A7: for k, j st k in ( dom G) & j in ( Seg m) holds (M * (k,j)) = (( Del (( Line (G,k)),i)) . j)

          proof

            let k, j;

            assume

             A8: k in ( dom G) & j in ( Seg m);

            then

             A9: (M . k) = ( Del (( Line (G,k)),i)) by MATRIX_0:def 13;

             [k, j] in ( Indices M) by A6, A8, ZFMISC_1: 87;

            then ex p be FinSequence of ( TOP-REAL 2) st p = (M . k) & (M * (k,j)) = (p . j) by MATRIX_0:def 5;

            hence thesis by A9;

          end;

          

           A10: for k, j st k in ( dom G) & j in ( Seg m) holds (M * (k,j)) = (( Line (G,k)) . j) or (M * (k,j)) = (( Line (G,k)) . (j + 1))

          proof

            let k, j;

            assume

             A11: k in ( dom G) & j in ( Seg m);

            then

             A12: (M * (k,j)) = (( Del (( Line (G,k)),i)) . j) by A7;

            

             A13: ( len ( Line (G,k))) = (m + 1) by A2, MATRIX_0:def 7;

            i in ( Seg ( len ( Line (G,k)))) by A1, MATRIX_0:def 7;

            then i in ( dom ( Line (G,k))) by FINSEQ_1:def 3;

            hence thesis by A11, A12, A13, SEQM_3: 44;

          end;

          set N = M;

          

           A14: for k st k in ( Seg m) holds ( Col (N,k)) = ( Col (G,k)) or ( Col (N,k)) = ( Col (G,(k + 1)))

          proof

            let k;

            assume

             A15: k in ( Seg m);

            then

             A16: 1 <= k & k <= m by FINSEQ_1: 1;

            m <= (m + 1) & k <= (k + 1) by NAT_1: 11;

            then k <= (m + 1) & 1 <= (k + 1) & (k + 1) <= (m + 1) by A16, XREAL_1: 6, XXREAL_0: 2;

            then

             A17: k in ( Seg ( width G)) & (k + 1) in ( Seg ( width G)) by A2, A16, FINSEQ_1: 1;

            

             A18: ( len ( Col (N,k))) = ( len N) & ( len ( Col (G,k))) = ( len G) & ( len ( Col (G,(k + 1)))) = ( len G) by MATRIX_0:def 8;

            now

              per cases ;

                suppose

                 A19: k < i;

                now

                  let j be Nat;

                  assume 1 <= j & j <= ( len ( Col (N,k)));

                  then

                   A20: j in ( dom N) by A18, FINSEQ_3: 25;

                  

                  hence (( Col (N,k)) . j) = (N * (j,k)) by MATRIX_0:def 8

                  .= (( Del (( Line (G,j)),i)) . k) by A7, A15, A20, A5

                  .= (( Line (G,j)) . k) by A19, FINSEQ_3: 110

                  .= (( Col (G,k)) . j) by A17, A20, A5, MATRIX_0: 42;

                end;

                hence thesis by A4, A18, FINSEQ_1: 14;

              end;

                suppose

                 A21: k >= i;

                now

                  let j be Nat;

                  assume 1 <= j & j <= ( len ( Col (N,k)));

                  then

                   A22: j in ( dom N) by A18, FINSEQ_3: 25;

                  

                   A23: ( len ( Line (G,j))) = (m + 1) by A2, MATRIX_0:def 7;

                  

                   A24: ( dom ( Line (G,j))) = ( Seg ( len ( Line (G,j)))) by FINSEQ_1:def 3;

                  

                  thus (( Col (N,k)) . j) = (N * (j,k)) by A22, MATRIX_0:def 8

                  .= (( Del (( Line (G,j)),i)) . k) by A7, A15, A22, A5

                  .= (( Line (G,j)) . (k + 1)) by A2, A16, A21, A23, A24, A1, FINSEQ_3: 111

                  .= (( Col (G,(k + 1))) . j) by A17, A22, A5, MATRIX_0: 42;

                end;

                hence thesis by A4, A18, FINSEQ_1: 14;

              end;

            end;

            hence thesis;

          end;

          thus M is X_equal-in-line

          proof

            let k;

            assume

             A25: k in ( dom M);

            then

             A26: ( X_axis ( Line (G,k))) is constant by Def3, A5;

            m <= (m + 1) by NAT_1: 11;

            then

             A27: ( Seg m) c= ( Seg ( width G)) by A2, FINSEQ_1: 5;

            reconsider L = ( Line (M,k)), lg = ( Line (G,k)) as FinSequence of ( TOP-REAL 2);

            set X = ( X_axis L), xg = ( X_axis lg);

            now

              let n,j be Nat such that

               A28: n in ( dom X) & j in ( dom X);

              

               A29: ( dom X) = ( Seg ( len X)) & ( len X) = ( len L) & ( len L) = ( width M) & ( dom xg) = ( Seg ( len xg)) & ( len xg) = ( len lg) & ( len lg) = ( width G) by Def1, FINSEQ_1:def 3, MATRIX_0:def 7;

              then

               A30: (L . n) = (M * (k,n)) & (L . j) = (M * (k,j)) & n in ( Seg m) & j in ( Seg m) by A28, A3, MATRIX_0:def 7;

              then

               A31: ((L . n) = (lg . n) or (L . n) = (lg . (n + 1))) & ((L . j) = (lg . j) or (L . j) = (lg . (j + 1))) by A10, A25, A5;

              n in ( dom L) & j in ( dom L) by A28, A29, FINSEQ_1:def 3;

              then (L . n) = (L /. n) & (L . j) = (L /. j) by PARTFUN1:def 6;

              then

               A32: (X . n) = ((M * (k,n)) `1 ) & (X . j) = ((M * (k,j)) `1 ) by A28, A30, Def1;

              1 <= n & n <= m & 1 <= j & j <= m by A4, A28, A29, FINSEQ_3: 25;

              then

               A33: n <= (n + 1) & (n + 1) <= (m + 1) & j <= (j + 1) & (j + 1) <= (m + 1) by NAT_1: 11, XREAL_1: 6;

              1 <= (n + 1) & 1 <= (j + 1) by NAT_1: 11;

              then

               A34: (n + 1) in ( Seg ( width G)) & (j + 1) in ( Seg ( width G)) & n in ( Seg ( width G)) & j in ( Seg ( width G)) by A2, A4, A27, A28, A29, A33, FINSEQ_3: 25;

              then

               A35: (lg . n) = (G * (k,n)) & (lg . (n + 1)) = (G * (k,(n + 1))) & (lg . j) = (G * (k,j)) & (lg . (j + 1)) = (G * (k,(j + 1))) by MATRIX_0:def 7;

              ( dom lg) = ( Seg ( len xg)) by A29, FINSEQ_1:def 3;

              then (lg . n) = (lg /. n) & (lg . (n + 1)) = (lg /. (n + 1)) & (lg . j) = (lg /. j) & (lg . (j + 1)) = (lg /. (j + 1)) by A29, A34, PARTFUN1:def 6;

              then (xg . n) = ((G * (k,n)) `1 ) & (xg . (n + 1)) = ((G * (k,(n + 1))) `1 ) & (xg . j) = ((G * (k,j)) `1 ) & (xg . (j + 1)) = ((G * (k,(j + 1))) `1 ) by A29, A34, A35, Def1;

              hence (X . n) = (X . j) by A26, A29, A30, A31, A32, A34, A35;

            end;

            hence ( X_axis ( Line (M,k))) is constant;

          end;

          thus M is Y_equal-in-column

          proof

            let k;

            assume

             A36: k in ( Seg ( width M));

            then

             A37: ( Col (M,k)) = ( Col (G,k)) or ( Col (M,k)) = ( Col (G,(k + 1))) by A4, A14;

            

             A38: 1 <= k & k <= m by A4, A36, FINSEQ_1: 1;

            m <= (m + 1) & k <= (k + 1) by NAT_1: 11;

            then k <= (m + 1) & 1 <= (k + 1) & (k + 1) <= (m + 1) by A38, XREAL_1: 6, XXREAL_0: 2;

            then k in ( Seg ( width G)) & (k + 1) in ( Seg ( width G)) by A2, A38, FINSEQ_1: 1;

            hence ( Y_axis ( Col (M,k))) is constant by A37, Def4;

          end;

          thus M is Y_increasing-in-line

          proof

            let k;

            reconsider L = ( Line (M,k)), lg = ( Line (G,k)) as FinSequence of ( TOP-REAL 2);

            set X = ( Y_axis L), xg = ( Y_axis lg);

            m <= (m + 1) by NAT_1: 11;

            then

             A39: ( Seg m) c= ( Seg ( width G)) by A2, FINSEQ_1: 5;

            assume

             A40: k in ( dom M);

            then

             A41: xg is increasing by Def5, A5;

            now

              let n, j such that

               A42: n in ( dom X) & j in ( dom X) & n < j;

              

               A43: ( dom X) = ( Seg ( len X)) & ( len X) = ( len L) & ( len L) = ( width M) & ( dom xg) = ( Seg ( len xg)) & ( len xg) = ( len lg) & ( len lg) = ( width G) by Def2, FINSEQ_1:def 3, MATRIX_0:def 7;

              then

               A44: (L . n) = (M * (k,n)) & (L . j) = (M * (k,j)) & n in ( Seg m) & j in ( Seg m) by A42, A3, MATRIX_0:def 7;

              ( dom L) = ( Seg ( len X)) by A43, FINSEQ_1:def 3;

              then (L . n) = (L /. n) & (L . j) = (L /. j) by A42, A43, PARTFUN1:def 6;

              then

               A45: (X . n) = ((M * (k,n)) `2 ) & (X . j) = ((M * (k,j)) `2 ) by A42, A44, Def2;

              

               A46: 1 <= n & n <= m & 1 <= j & j <= m by A4, A42, A43, FINSEQ_3: 25;

              then

               A47: n <= (n + 1) & (n + 1) <= (m + 1) & j <= (j + 1) & (j + 1) <= (m + 1) by NAT_1: 11, XREAL_1: 6;

              1 <= (n + 1) & 1 <= (j + 1) by NAT_1: 11;

              then

               A48: (n + 1) in ( Seg ( width G)) & (j + 1) in ( Seg ( width G)) & n in ( Seg ( width G)) & j in ( Seg ( width G)) by A2, A4, A39, A42, A43, A47, FINSEQ_3: 25;

              then

               A49: (lg . n) = (G * (k,n)) & (lg . (n + 1)) = (G * (k,(n + 1))) & (lg . j) = (G * (k,j)) & (lg . (j + 1)) = (G * (k,(j + 1))) by MATRIX_0:def 7;

              ( dom lg) = ( Seg ( len xg)) by A43, FINSEQ_1:def 3;

              then (lg . n) = (lg /. n) & (lg . (n + 1)) = (lg /. (n + 1)) & (lg . j) = (lg /. j) & (lg . (j + 1)) = (lg /. (j + 1)) by A43, A48, PARTFUN1:def 6;

              then

               A50: (xg . n) = ((G * (k,n)) `2 ) & (xg . (n + 1)) = ((G * (k,(n + 1))) `2 ) & (xg . j) = ((G * (k,j)) `2 ) & (xg . (j + 1)) = ((G * (k,(j + 1))) `2 ) by A43, A48, A49, Def2;

              set r = (X . n), s = (X . j);

              

               A51: ( dom lg) = ( Seg ( len lg)) by FINSEQ_1:def 3;

              per cases ;

                suppose

                 A52: j < i;

                then

                 A53: n < i by A42, XXREAL_0: 2;

                

                 A54: (M * (k,n)) = (( Del (lg,i)) . n) by A4, A7, A40, A42, A43, A5

                .= (G * (k,n)) by A49, A53, FINSEQ_3: 110;

                (M * (k,j)) = (( Del (lg,i)) . j) by A4, A7, A40, A42, A43, A5

                .= (G * (k,j)) by A49, A52, FINSEQ_3: 110;

                hence r < s by A4, A39, A41, A42, A43, A45, A50, A54;

              end;

                suppose

                 A55: j >= i;

                

                 A56: (M * (k,j)) = (( Del (lg,i)) . j) by A4, A7, A40, A42, A43, A5

                .= (G * (k,(j + 1))) by A2, A43, A46, A49, A51, A55, A1, FINSEQ_3: 111;

                now

                  per cases ;

                    suppose

                     A57: n < i;

                    j <= (j + 1) by NAT_1: 11;

                    then

                     A58: n < (j + 1) by A42, XXREAL_0: 2;

                    (M * (k,n)) = (( Del (lg,i)) . n) by A4, A7, A40, A42, A43, A5

                    .= (G * (k,n)) by A49, A57, FINSEQ_3: 110;

                    hence r < s by A41, A43, A45, A48, A50, A56, A58;

                  end;

                    suppose

                     A59: n >= i;

                    

                     A60: (n + 1) < (j + 1) by A42, XREAL_1: 6;

                    (M * (k,n)) = (( Del (lg,i)) . n) by A4, A7, A40, A42, A43, A5

                    .= (G * (k,(n + 1))) by A2, A43, A46, A49, A51, A59, A1, FINSEQ_3: 111;

                    hence r < s by A41, A43, A45, A48, A50, A56, A60;

                  end;

                end;

                hence r < s;

              end;

            end;

            hence ( Y_axis ( Line (M,k))) is increasing;

          end;

          let k;

          assume

           A61: k in ( Seg ( width M));

          then

           A62: ( Col (M,k)) = ( Col (G,k)) or ( Col (M,k)) = ( Col (G,(k + 1))) by A4, A14;

          

           A63: 1 <= k & k <= m by A4, A61, FINSEQ_1: 1;

          m <= (m + 1) & k <= (k + 1) by NAT_1: 11;

          then k <= (m + 1) & 1 <= (k + 1) & (k + 1) <= (m + 1) by A63, XREAL_1: 6, XXREAL_0: 2;

          then k in ( Seg ( width G)) & (k + 1) in ( Seg ( width G)) by A2, A63, FINSEQ_1: 1;

          hence ( X_axis ( Col (M,k))) is increasing by A62, Def6;

        end;

      end;

    end

    ::$Canceled

    theorem :: GOBOARD1:12

    i in ( Seg ( width G)) & ( width G) > 1 & n in ( dom G) & m in ( Seg ( width ( DelCol (G,i)))) implies (( DelCol (G,i)) * (n,m)) = (( Del (( Line (G,n)),i)) . m) by MATRIX_0: 66;

    theorem :: GOBOARD1:13

    

     Th6: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & 1 <= k & k < i implies ( Col (( DelCol (G,i)),k)) = ( Col (G,k)) & k in ( Seg ( width ( DelCol (G,i)))) & k in ( Seg ( width G)) by MATRIX_0: 67;

    theorem :: GOBOARD1:14

    i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & i <= k & k <= m implies ( Col (( DelCol (G,i)),k)) = ( Col (G,(k + 1))) & k in ( Seg ( width ( DelCol (G,i)))) & (k + 1) in ( Seg ( width G)) by MATRIX_0: 68;

    theorem :: GOBOARD1:15

    

     Th8: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & n in ( dom G) & 1 <= k & k < i implies (( DelCol (G,i)) * (n,k)) = (G * (n,k)) & k in ( Seg ( width G)) by MATRIX_0: 69;

    theorem :: GOBOARD1:16

    

     Th9: i in ( Seg ( width G)) & ( width G) = (m + 1) & m > 0 & n in ( dom G) & i <= k & k <= m implies (( DelCol (G,i)) * (n,k)) = (G * (n,(k + 1))) & (k + 1) in ( Seg ( width G)) by MATRIX_0: 70;

    theorem :: GOBOARD1:17

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) implies ( Col (( DelCol (G,1)),k)) = ( Col (G,(k + 1))) & k in ( Seg ( width ( DelCol (G,1)))) & (k + 1) in ( Seg ( width G)) by MATRIX_0: 71;

    theorem :: GOBOARD1:18

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) & n in ( dom G) implies (( DelCol (G,1)) * (n,k)) = (G * (n,(k + 1))) & 1 in ( Seg ( width G)) by MATRIX_0: 72;

    theorem :: GOBOARD1:19

    ( width G) = (m + 1) & m > 0 & k in ( Seg m) implies ( Col (( DelCol (G,( width G))),k)) = ( Col (G,k)) & k in ( Seg ( width ( DelCol (G,( width G))))) by MATRIX_0: 73;

    theorem :: GOBOARD1:20

    

     Th13: ( width G) = (m + 1) & m > 0 & k in ( Seg m) & n in ( dom G) implies k in ( Seg ( width G)) & (( DelCol (G,( width G))) * (n,k)) = (G * (n,k)) & ( width G) in ( Seg ( width G)) by MATRIX_0: 74;

    theorem :: GOBOARD1:21

    ( rng f) misses ( rng ( Col (G,i))) & (f /. n) in ( rng ( Line (G,m))) & n in ( dom f) & i in ( Seg ( width G)) & m in ( dom G) & ( width G) > 1 implies (f /. n) in ( rng ( Line (( DelCol (G,i)),m))) by MATRIX_0: 75;

    reserve D for set,

f for FinSequence of D,

M for Matrix of D;

    definition

      ::$Canceled

      let D, f, M;

      :: GOBOARD1:def9

      pred f is_sequence_on M means (for n st n in ( dom f) holds ex i, j st [i, j] in ( Indices M) & (f /. n) = (M * (i,j))) & for n st n in ( dom f) & (n + 1) in ( dom f) holds for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f /. n) = (M * (m,k)) & (f /. (n + 1)) = (M * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1;

    end

    theorem :: GOBOARD1:22

    (m in ( dom f) implies 1 <= ( len (f | m))) & (f is_sequence_on M implies (f | m) is_sequence_on M)

    proof

      set g = (f | m);

      thus m in ( dom f) implies 1 <= ( len (f | m))

      proof

        assume m in ( dom f);

        then 1 <= m & m <= ( len f) by FINSEQ_3: 25;

        hence thesis by FINSEQ_1: 59;

      end;

      assume

       A1: f is_sequence_on M;

      per cases ;

        suppose

         A2: m < 1;

        m = 0 by A2, NAT_1: 14;

        hence thesis;

      end;

        suppose m >= ( len f);

        hence thesis by A1, FINSEQ_1: 58;

      end;

        suppose

         A3: 1 <= m & m < ( len f);

        

         A4: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

        

         A5: m in ( dom f) & ( len g) = m by A3, FINSEQ_1: 59, FINSEQ_3: 25;

         A6:

        now

          let n;

          assume

           A7: n in ( dom g) & (n + 1) in ( dom g);

          then

           A8: n in ( dom f) & (n + 1) in ( dom f) by A4, A5, FINSEQ_4: 71;

          let i1,i2,j1,j2 be Nat;

          assume

           A9: [i1, i2] in ( Indices M) & [j1, j2] in ( Indices M) & (g /. n) = (M * (i1,i2)) & (g /. (n + 1)) = (M * (j1,j2));

          (g /. n) = (f /. n) & (g /. (n + 1)) = (f /. (n + 1)) by A4, A5, A7, FINSEQ_4: 71;

          hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A1, A8, A9;

        end;

        now

          let n;

          assume

           A10: n in ( dom g);

          then n in ( dom f) by A4, A5, FINSEQ_4: 71;

          then

          consider i, j such that

           A11: [i, j] in ( Indices M) & (f /. n) = (M * (i,j)) by A1;

          take i, j;

          thus [i, j] in ( Indices M) & (g /. n) = (M * (i,j)) by A4, A5, A10, A11, FINSEQ_4: 71;

        end;

        hence thesis by A6;

      end;

    end;

    theorem :: GOBOARD1:23

    (for n st n in ( dom f1) holds ex i, j st [i, j] in ( Indices M) & (f1 /. n) = (M * (i,j))) & (for n st n in ( dom f2) holds ex i, j st [i, j] in ( Indices M) & (f2 /. n) = (M * (i,j))) implies for n st n in ( dom (f1 ^ f2)) holds ex i, j st [i, j] in ( Indices M) & ((f1 ^ f2) /. n) = (M * (i,j))

    proof

      assume that

       A1: for n st n in ( dom f1) holds ex i, j st [i, j] in ( Indices M) & (f1 /. n) = (M * (i,j)) and

       A2: for n st n in ( dom f2) holds ex i, j st [i, j] in ( Indices M) & (f2 /. n) = (M * (i,j));

      let n such that

       A3: n in ( dom (f1 ^ f2));

      per cases by A3, FINSEQ_1: 25;

        suppose

         A4: n in ( dom f1);

        then

        consider i, j such that

         A5: [i, j] in ( Indices M) and

         A6: (f1 /. n) = (M * (i,j)) by A1;

        take i, j;

        thus [i, j] in ( Indices M) by A5;

        thus thesis by A4, A6, FINSEQ_4: 68;

      end;

        suppose ex m be Nat st m in ( dom f2) & n = (( len f1) + m);

        then

        consider m be Nat such that

         A7: m in ( dom f2) and

         A8: n = (( len f1) + m);

        consider i, j such that

         A9: [i, j] in ( Indices M) and

         A10: (f2 /. m) = (M * (i,j)) by A2, A7;

        take i, j;

        thus [i, j] in ( Indices M) by A9;

        thus thesis by A7, A8, A10, FINSEQ_4: 69;

      end;

    end;

    theorem :: GOBOARD1:24

    (for n st n in ( dom f1) & (n + 1) in ( dom f1) holds for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f1 /. n) = (M * (m,k)) & (f1 /. (n + 1)) = (M * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1) & (for n st n in ( dom f2) & (n + 1) in ( dom f2) holds for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f2 /. n) = (M * (m,k)) & (f2 /. (n + 1)) = (M * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1) & (for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f1 /. ( len f1)) = (M * (m,k)) & (f2 /. 1) = (M * (i,j)) & ( len f1) in ( dom f1) & 1 in ( dom f2) holds ( |.(m - i).| + |.(k - j).|) = 1) implies for n st n in ( dom (f1 ^ f2)) & (n + 1) in ( dom (f1 ^ f2)) holds for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & ((f1 ^ f2) /. n) = (M * (m,k)) & ((f1 ^ f2) /. (n + 1)) = (M * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1

    proof

      assume that

       A1: for n st n in ( dom f1) & (n + 1) in ( dom f1) holds for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f1 /. n) = (M * (m,k)) & (f1 /. (n + 1)) = (M * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 and

       A2: for n st n in ( dom f2) & (n + 1) in ( dom f2) holds for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f2 /. n) = (M * (m,k)) & (f2 /. (n + 1)) = (M * (i,j)) holds ( |.(m - i).| + |.(k - j).|) = 1 and

       A3: for m, k, i, j st [m, k] in ( Indices M) & [i, j] in ( Indices M) & (f1 /. ( len f1)) = (M * (m,k)) & (f2 /. 1) = (M * (i,j)) & ( len f1) in ( dom f1) & 1 in ( dom f2) holds ( |.(m - i).| + |.(k - j).|) = 1;

      let n such that

       A4: n in ( dom (f1 ^ f2)) and

       A5: (n + 1) in ( dom (f1 ^ f2));

      let m, k, i, j such that

       A6: [m, k] in ( Indices M) & [i, j] in ( Indices M) and

       A7: ((f1 ^ f2) /. n) = (M * (m,k)) and

       A8: ((f1 ^ f2) /. (n + 1)) = (M * (i,j));

      

       A9: ( dom f1) = ( Seg ( len f1)) by FINSEQ_1:def 3;

      per cases by A4, FINSEQ_1: 25;

        suppose

         A10: n in ( dom f1);

        then

         A11: (f1 /. n) = (M * (m,k)) by A7, FINSEQ_4: 68;

        now

          per cases by A5, FINSEQ_1: 25;

            suppose

             A12: (n + 1) in ( dom f1);

            then (f1 /. (n + 1)) = (M * (i,j)) by A8, FINSEQ_4: 68;

            hence thesis by A1, A6, A10, A11, A12;

          end;

            suppose ex m be Nat st m in ( dom f2) & (n + 1) = (( len f1) + m);

            then

            consider mm be Nat such that

             A13: mm in ( dom f2) and

             A14: (n + 1) = (( len f1) + mm);

            1 <= mm by A13, FINSEQ_3: 25;

            then

             A15: 0 <= (mm - 1) by XREAL_1: 48;

            (( len f1) + (mm - 1)) <= (( len f1) + 0 ) by A9, A10, A14, FINSEQ_1: 1;

            then

             A16: (mm - 1) = 0 by A15, XREAL_1: 6;

            then (M * (i,j)) = (f2 /. 1) & (M * (m,k)) = (f1 /. ( len f1)) by A7, A8, A10, A13, A14, FINSEQ_4: 68, FINSEQ_4: 69;

            hence thesis by A3, A6, A10, A13, A14, A16;

          end;

        end;

        hence thesis;

      end;

        suppose ex m be Nat st m in ( dom f2) & n = (( len f1) + m);

        then

        consider mm be Nat such that

         A17: mm in ( dom f2) and

         A18: n = (( len f1) + mm);

        

         A19: (M * (m,k)) = (f2 /. mm) by A7, A17, A18, FINSEQ_4: 69;

        

         A20: ((( len f1) + mm) + 1) = (( len f1) + (mm + 1));

        (n + 1) <= ( len (f1 ^ f2)) by A5, FINSEQ_3: 25;

        then ((( len f1) + mm) + 1) <= (( len f1) + ( len f2)) by A18, FINSEQ_1: 22;

        then 1 <= (mm + 1) & (mm + 1) <= ( len f2) by A20, NAT_1: 11, XREAL_1: 6;

        then

         A21: (mm + 1) in ( dom f2) by FINSEQ_3: 25;

        (M * (i,j)) = ((f1 ^ f2) /. (( len f1) + (mm + 1))) by A8, A18

        .= (f2 /. (mm + 1)) by A21, FINSEQ_4: 69;

        hence thesis by A2, A6, A17, A21, A19;

      end;

    end;

    reserve f for FinSequence of ( TOP-REAL 2);

    theorem :: GOBOARD1:25

    f is_sequence_on G & i in ( Seg ( width G)) & ( rng f) misses ( rng ( Col (G,i))) & ( width G) > 1 implies f is_sequence_on ( DelCol (G,i))

    proof

      set D = ( DelCol (G,i));

      assume that

       A1: f is_sequence_on G and

       A2: i in ( Seg ( width G)) and

       A3: ( rng f) misses ( rng ( Col (G,i))) and

       A4: ( width G) > 1;

      

       A5: ( len G) = ( len D) by MATRIX_0:def 13;

      

       A6: ( Indices D) = [:( dom D), ( Seg ( width D)):] by MATRIX_0:def 4;

      

       A7: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      

       A8: ( dom G) = ( Seg ( len G)) & ( dom D) = ( Seg ( len D)) by FINSEQ_1:def 3;

      consider M be Nat such that

       A9: ( width G) = (M + 1) and

       A10: M > 0 by A4, SEQM_3: 43;

      

       A11: ( width D) = M by A2, A9, MATRIX_0: 63;

       A12:

      now

        let n such that

         A13: n in ( dom f) & (n + 1) in ( dom f);

        let i1,i2,j1,j2 be Nat;

        assume that

         A14: [i1, i2] in ( Indices D) and

         A15: [j1, j2] in ( Indices D) and

         A16: (f /. n) = (D * (i1,i2)) & (f /. (n + 1)) = (D * (j1,j2));

        

         A17: i1 in ( dom D) by A6, A14, ZFMISC_1: 87;

        

         A18: i2 in ( Seg ( width D)) by A6, A14, ZFMISC_1: 87;

        then

         A19: 1 <= i2 by FINSEQ_1: 1;

        

         A20: i2 <= M by A11, A18, FINSEQ_1: 1;

        then 1 <= (i2 + 1) & (i2 + 1) <= (M + 1) by NAT_1: 11, XREAL_1: 6;

        then (i2 + 1) in ( Seg (M + 1)) by FINSEQ_1: 1;

        then

         A21: [i1, (i2 + 1)] in ( Indices G) by A5, A9, A8, A7, A17, ZFMISC_1: 87;

        

         A22: j1 in ( dom D) by A6, A15, ZFMISC_1: 87;

        

         A23: j2 in ( Seg ( width D)) by A6, A15, ZFMISC_1: 87;

        then

         A24: 1 <= j2 by FINSEQ_1: 1;

        M <= (M + 1) by NAT_1: 11;

        then

         A25: ( Seg ( width D)) c= ( Seg ( width G)) by A9, A11, FINSEQ_1: 5;

        then

         A26: [j1, j2] in ( Indices G) by A5, A8, A7, A22, A23, ZFMISC_1: 87;

        

         A27: j2 <= M by A11, A23, FINSEQ_1: 1;

        then 1 <= (j2 + 1) & (j2 + 1) <= (M + 1) by NAT_1: 11, XREAL_1: 6;

        then (j2 + 1) in ( Seg (M + 1)) by FINSEQ_1: 1;

        then

         A28: [j1, (j2 + 1)] in ( Indices G) by A5, A9, A8, A7, A22, ZFMISC_1: 87;

        

         A29: [i1, i2] in ( Indices G) by A5, A8, A7, A17, A18, A25, ZFMISC_1: 87;

        now

          per cases ;

            case i2 < i & j2 < i;

            then (f /. n) = (G * (i1,i2)) & (f /. (n + 1)) = (G * (j1,j2)) by A2, A5, A9, A10, A8, A16, A17, A22, A19, A24, Th8;

            hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A1, A13, A29, A26;

          end;

            case

             A30: i <= i2 & j2 < i;

            i2 <= (i2 + 1) by NAT_1: 11;

            then i <= (i2 + 1) by A30, XXREAL_0: 2;

            then

             A31: j2 < (i2 + 1) by A30, XXREAL_0: 2;

            then (j2 + 1) <= (i2 + 1) by NAT_1: 13;

            then

             A32: 1 <= ((i2 + 1) - j2) by XREAL_1: 19;

            (f /. n) = (G * (i1,(i2 + 1))) & (f /. (n + 1)) = (G * (j1,j2)) by A2, A5, A9, A8, A16, A17, A22, A20, A24, A30, Th8, Th9;

            then

             A33: 1 = ( |.(i1 - j1).| + |.((i2 + 1) - j2).|) by A1, A13, A26, A21;

             0 < ((i2 + 1) - j2) by A31, XREAL_1: 50;

            then

             A34: |.((i2 + 1) - j2).| = ((i2 + 1) - j2) by ABSVALUE:def 1;

             0 <= |.(i1 - j1).| by COMPLEX1: 46;

            then ( 0 + ((i2 + 1) - j2)) <= 1 by A33, A34, XREAL_1: 7;

            then ((i2 + 1) - j2) = 1 by A32, XXREAL_0: 1;

            hence contradiction by A30;

          end;

            case

             A35: i2 < i & i <= j2;

            j2 <= (j2 + 1) by NAT_1: 11;

            then i <= (j2 + 1) by A35, XXREAL_0: 2;

            then

             A36: i2 < (j2 + 1) by A35, XXREAL_0: 2;

            then (i2 + 1) <= (j2 + 1) by NAT_1: 13;

            then

             A37: 1 <= ((j2 + 1) - i2) by XREAL_1: 19;

            (f /. n) = (G * (i1,i2)) & (f /. (n + 1)) = (G * (j1,(j2 + 1))) by A2, A5, A9, A8, A16, A17, A22, A19, A27, A35, Th8, Th9;

            

            then

             A38: 1 = ( |.(i1 - j1).| + |.(i2 - (j2 + 1)).|) by A1, A13, A29, A28

            .= ( |.(i1 - j1).| + |.( - ((j2 + 1) - i2)).|)

            .= ( |.(i1 - j1).| + |.((j2 + 1) - i2).|) by COMPLEX1: 52;

             0 < ((j2 + 1) - i2) by A36, XREAL_1: 50;

            then

             A39: |.((j2 + 1) - i2).| = ((j2 + 1) - i2) by ABSVALUE:def 1;

             0 <= |.(i1 - j1).| by COMPLEX1: 46;

            then ( 0 + ((j2 + 1) - i2)) <= 1 by A38, A39, XREAL_1: 7;

            then ((j2 + 1) - i2) = 1 by A37, XXREAL_0: 1;

            hence contradiction by A35;

          end;

            case i <= i2 & i <= j2;

            then (f /. n) = (G * (i1,(i2 + 1))) & (f /. (n + 1)) = (G * (j1,(j2 + 1))) by A2, A5, A9, A10, A8, A16, A17, A22, A20, A27, Th9;

            

            hence 1 = ( |.(i1 - j1).| + |.((i2 + 1) - (j2 + 1)).|) by A1, A13, A21, A28

            .= ( |.(i1 - j1).| + |.(i2 - j2).|);

          end;

        end;

        hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1;

      end;

      

       A40: 1 <= i by A2, FINSEQ_1: 1;

      

       A41: i <= ( width G) by A2, FINSEQ_1: 1;

      now

        let n;

        assume

         A42: n in ( dom f);

        then

        consider m, k such that

         A43: [m, k] in ( Indices G) and

         A44: (f /. n) = (G * (m,k)) by A1;

        take m;

        

         A45: m in ( dom G) by A7, A43, ZFMISC_1: 87;

        

         A46: k in ( Seg ( width G)) by A7, A43, ZFMISC_1: 87;

        then

         A47: 1 <= k by FINSEQ_1: 1;

        

         A48: k <= (M + 1) by A9, A46, FINSEQ_1: 1;

        now

          per cases ;

            suppose

             A49: k < i;

            take k;

            k < ( width G) by A41, A49, XXREAL_0: 2;

            then k <= M by A9, NAT_1: 13;

            then k in ( Seg M) by A47, FINSEQ_1: 1;

            hence [m, k] in ( Indices D) & (f /. n) = (D * (m,k)) by A2, A5, A9, A10, A11, A8, A6, A44, A45, A47, A49, Th8, ZFMISC_1: 87;

          end;

            suppose i <= k;

            then

             A50: i < k by A3, A42, A44, A45, MATRIX_0: 43, XXREAL_0: 1;

            then (k - 1) in NAT by A40, INT_1: 5, XXREAL_0: 2;

            then

            reconsider l = (k - 1) as Nat;

            take l;

            

             A51: l <= M by A48, XREAL_1: 20;

            (i + 1) <= k by A50, NAT_1: 13;

            then

             A52: i <= (k - 1) by XREAL_1: 19;

            then 1 <= l by A40, XXREAL_0: 2;

            then

             A53: l in ( Seg M) by A51, FINSEQ_1: 1;

            (D * (m,l)) = (G * (m,(l + 1))) by A2, A9, A40, A45, A52, A51, Th9;

            hence [m, l] in ( Indices D) & (f /. n) = (D * (m,l)) by A5, A11, A8, A6, A44, A45, A53, ZFMISC_1: 87;

          end;

        end;

        hence ex k st [m, k] in ( Indices D) & (f /. n) = (D * (m,k));

      end;

      hence thesis by A12;

    end;

    theorem :: GOBOARD1:26

    

     Th19: f is_sequence_on G & i in ( dom f) implies ex n st n in ( dom G) & (f /. i) in ( rng ( Line (G,n)))

    proof

      assume f is_sequence_on G & i in ( dom f);

      then

      consider n, m such that

       A1: [n, m] in ( Indices G) and

       A2: (f /. i) = (G * (n,m));

      set L = ( Line (G,n));

      take n;

      

       A3: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      hence n in ( dom G) by A1, ZFMISC_1: 87;

      

       A4: m in ( Seg ( width G)) by A1, A3, ZFMISC_1: 87;

      ( len L) = ( width G) by MATRIX_0:def 7;

      then

       A5: m in ( dom L) by A4, FINSEQ_1:def 3;

      (L . m) = (f /. i) by A2, A4, MATRIX_0:def 7;

      hence thesis by A5, FUNCT_1:def 3;

    end;

    theorem :: GOBOARD1:27

    

     Th20: f is_sequence_on G & i in ( dom f) & (i + 1) in ( dom f) & n in ( dom G) & (f /. i) in ( rng ( Line (G,n))) implies (f /. (i + 1)) in ( rng ( Line (G,n))) or for k st (f /. (i + 1)) in ( rng ( Line (G,k))) & k in ( dom G) holds |.(n - k).| = 1

    proof

      assume that

       A1: f is_sequence_on G and

       A2: i in ( dom f) and

       A3: (i + 1) in ( dom f) and

       A4: n in ( dom G) & (f /. i) in ( rng ( Line (G,n)));

      consider j1,j2 be Nat such that

       A5: [j1, j2] in ( Indices G) and

       A6: (f /. (i + 1)) = (G * (j1,j2)) by A1, A3;

      

       A7: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      then

       A8: j1 in ( dom G) by A5, ZFMISC_1: 87;

      consider i1,i2 be Nat such that

       A9: [i1, i2] in ( Indices G) and

       A10: (f /. i) = (G * (i1,i2)) by A1, A2;

      

       A11: i2 in ( Seg ( width G)) by A9, A7, ZFMISC_1: 87;

      ( len ( Line (G,i1))) = ( width G) by MATRIX_0:def 7;

      then

       A12: i2 in ( dom ( Line (G,i1))) by A11, FINSEQ_1:def 3;

      (( Line (G,i1)) . i2) = (f /. i) by A10, A11, MATRIX_0:def 7;

      then

       A13: (f /. i) in ( rng ( Line (G,i1))) by A12, FUNCT_1:def 3;

      i1 in ( dom G) by A9, A7, ZFMISC_1: 87;

      then i1 = n by A4, A13, Th2;

      then

       A14: ( |.(n - j1).| + |.(i2 - j2).|) = 1 by A1, A2, A3, A9, A10, A5, A6;

      

       A15: j2 in ( Seg ( width G)) by A5, A7, ZFMISC_1: 87;

      ( len ( Line (G,j1))) = ( width G) by MATRIX_0:def 7;

      then

       A16: j2 in ( dom ( Line (G,j1))) by A15, FINSEQ_1:def 3;

      

       A17: (( Line (G,j1)) . j2) = (f /. (i + 1)) by A6, A15, MATRIX_0:def 7;

      then

       A18: (f /. (i + 1)) in ( rng ( Line (G,j1))) by A16, FUNCT_1:def 3;

      now

        per cases by A14, SEQM_3: 42;

          suppose |.(n - j1).| = 1 & i2 = j2;

          hence thesis by A8, A18, Th2;

        end;

          suppose |.(i2 - j2).| = 1 & n = j1;

          hence thesis by A17, A16, FUNCT_1:def 3;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD1:28

    

     Th21: 1 <= ( len f) & (f /. ( len f)) in ( rng ( Line (G,( len G)))) & f is_sequence_on G & i in ( dom G) & (i + 1) in ( dom G) & m in ( dom f) & (f /. m) in ( rng ( Line (G,i))) & (for k st k in ( dom f) & (f /. k) in ( rng ( Line (G,i))) holds k <= m) implies (m + 1) in ( dom f) & (f /. (m + 1)) in ( rng ( Line (G,(i + 1))))

    proof

      assume that

       A1: 1 <= ( len f) and

       A2: (f /. ( len f)) in ( rng ( Line (G,( len G)))) and

       A3: f is_sequence_on G and

       A4: i in ( dom G) and

       A5: (i + 1) in ( dom G) and

       A6: m in ( dom f) and

       A7: (f /. m) in ( rng ( Line (G,i))) and

       A8: for k st k in ( dom f) & (f /. k) in ( rng ( Line (G,i))) holds k <= m;

      reconsider p = (f /. ( len f)), q = (f /. m) as Point of ( TOP-REAL 2);

      defpred P[ Nat, set] means $2 in ( dom G) & for k st k = $2 holds (f /. $1) in ( rng ( Line (G,k)));

      

       A9: for n st n in ( dom f) holds ex k st k in ( dom G) & (f /. n) in ( rng ( Line (G,k)))

      proof

        assume not thesis;

        then

        consider n such that

         A10: n in ( dom f) and

         A11: for k st k in ( dom G) holds not (f /. n) in ( rng ( Line (G,k)));

        consider i, j such that

         A12: [i, j] in ( Indices G) and

         A13: (f /. n) = (G * (i,j)) by A3, A10;

        

         A14: [i, j] in [:( dom G), ( Seg ( width G)):] by A12, MATRIX_0:def 4;

        then i in ( dom G) by ZFMISC_1: 87;

        then

         A15: not (f /. n) in ( rng ( Line (G,i))) by A11;

        

         A16: j in ( Seg ( width G)) by A14, ZFMISC_1: 87;

        then j in ( Seg ( len ( Line (G,i)))) by MATRIX_0:def 7;

        then

         A17: j in ( dom ( Line (G,i))) by FINSEQ_1:def 3;

        (( Line (G,i)) . j) = (G * (i,j)) by A16, MATRIX_0:def 7;

        hence contradiction by A13, A15, A17, FUNCT_1:def 3;

      end;

      

       A18: for n be Nat st n in ( Seg ( len f)) holds ex r be Element of REAL st P[n, r]

      proof

        let n be Nat;

        assume n in ( Seg ( len f));

        then n in ( dom f) by FINSEQ_1:def 3;

        then

        consider k such that

         A19: k in ( dom G) and

         A20: (f /. n) in ( rng ( Line (G,k))) by A9;

        reconsider r = k as Element of REAL by XREAL_0:def 1;

        take r;

        thus r in ( dom G) by A19;

        let m;

        assume m = r;

        hence thesis by A20;

      end;

      consider v such that

       A21: ( dom v) = ( Seg ( len f)) and

       A22: for n be Nat st n in ( Seg ( len f)) holds P[n, (v . n)] from FINSEQ_1:sch 5( A18);

      

       A23: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      

       A24: for k st k in ( dom v) & (v . k) = i holds k <= m

      proof

        let k;

        assume that

         A25: k in ( dom v) and

         A26: (v . k) = i;

        (f /. k) in ( rng ( Line (G,i))) by A21, A22, A25, A26;

        hence thesis by A8, A21, A23, A25;

      end;

      

       A27: ( rng v) c= ( dom G)

      proof

        let x be object;

        assume x in ( rng v);

        then ex y be Nat st y in ( dom v) & (v . y) = x by FINSEQ_2: 10;

        hence thesis by A21, A22;

      end;

      

       A28: ( len v) = ( len f) by A21, FINSEQ_1:def 3;

      

       A29: for k st 1 <= k & k <= (( len v) - 1) holds for r, s st r = (v . k) & s = (v . (k + 1)) holds |.(r - s).| = 1 or r = s

      proof

        let k;

        assume that

         A30: 1 <= k and

         A31: k <= (( len v) - 1);

        

         A32: (k + 1) <= ( len v) by A31, XREAL_1: 19;

        let r, s;

        assume that

         A33: r = (v . k) and

         A34: s = (v . (k + 1));

        1 <= (k + 1) by NAT_1: 11;

        then

         A35: (k + 1) in ( dom f) by A28, A32, FINSEQ_3: 25;

        then

         A36: s in ( rng v) by A21, A23, A34, FUNCT_1:def 3;

        then

         A37: s in ( dom G) by A27;

        k <= (k + 1) by NAT_1: 11;

        then k <= ( len f) by A28, A32, XXREAL_0: 2;

        then

         A38: k in ( dom f) by A30, FINSEQ_3: 25;

        then

         A39: r in ( rng v) by A21, A23, A33, FUNCT_1:def 3;

        then r in ( dom G) by A27;

        then

        reconsider n1 = r, n2 = s as Element of NAT by A37;

        set L1 = ( Line (G,n1)), L2 = ( Line (G,n2));

        (f /. k) in ( rng L1) by A22, A23, A38, A33;

        then

        consider x be Nat such that

         A40: x in ( dom L1) and

         A41: (L1 . x) = (f /. k) by FINSEQ_2: 10;

        

         A42: ( dom L1) = ( Seg ( len L1)) & ( len L1) = ( width G) by FINSEQ_1:def 3, MATRIX_0:def 7;

        then

         A43: (f /. k) = (G * (n1,x)) by A40, A41, MATRIX_0:def 7;

        (f /. (k + 1)) in ( rng L2) by A22, A23, A35, A34;

        then

        consider y be Nat such that

         A44: y in ( dom L2) and

         A45: (L2 . y) = (f /. (k + 1)) by FINSEQ_2: 10;

        reconsider x, y as Element of NAT by ORDINAL1:def 12;

         [n1, x] in [:( dom G), ( Seg ( width G)):] by A27, A39, A40, A42, ZFMISC_1: 87;

        then

         A46: [n1, x] in ( Indices G) by MATRIX_0:def 4;

        

         A47: ( Seg ( len L2)) = ( dom L2) & ( len L2) = ( width G) by FINSEQ_1:def 3, MATRIX_0:def 7;

        then [n2, y] in [:( dom G), ( Seg ( width G)):] by A27, A36, A44, ZFMISC_1: 87;

        then

         A48: [n2, y] in ( Indices G) by MATRIX_0:def 4;

        (f /. (k + 1)) = (G * (n2,y)) by A47, A44, A45, MATRIX_0:def 7;

        then ( |.(n1 - n2).| + |.(x - y).|) = 1 by A3, A38, A35, A43, A46, A48;

        hence thesis by SEQM_3: 42;

      end;

      

       A49: (v . m) = i

      proof

        

         A50: (v . m) in ( dom G) by A6, A22, A23;

        then

        reconsider k = (v . m) as Element of NAT ;

        assume

         A51: (v . m) <> i;

        q in ( rng ( Line (G,k))) by A6, A22, A23;

        hence contradiction by A4, A7, A51, A50, Th2;

      end;

      1 <= m & m <= ( len f) by A6, FINSEQ_3: 25;

      then 1 <= ( len f) by XXREAL_0: 2;

      then

       A52: ( len f) in ( dom f) by FINSEQ_3: 25;

      

       A53: (v . ( len v)) = ( len G)

      proof

         0 < ( len G) by MATRIX_0: 44;

        then ( 0 + 1) <= ( len G) by NAT_1: 13;

        then

         A54: ( len G) in ( dom G) by FINSEQ_3: 25;

        

         A55: (v . ( len v)) in ( dom G) by A22, A28, A23, A52;

        then

        reconsider k = (v . ( len v)) as Element of NAT ;

        assume

         A56: (v . ( len v)) <> ( len G);

        p in ( rng ( Line (G,k))) by A22, A28, A23, A52;

        hence contradiction by A2, A56, A55, A54, Th2;

      end;

      

       A57: ( dom G) = ( Seg ( len G)) & v <> {} by A1, A21, FINSEQ_1:def 3;

      hence (m + 1) in ( dom f) by A4, A5, A6, A21, A23, A27, A53, A29, A49, A24, SEQM_3: 45;

      (m + 1) in ( dom v) & (v . (m + 1)) = (i + 1) by A4, A5, A6, A21, A23, A57, A27, A53, A29, A49, A24, SEQM_3: 45;

      hence thesis by A21, A22;

    end;

    theorem :: GOBOARD1:29

    1 <= ( len f) & (f /. 1) in ( rng ( Line (G,1))) & (f /. ( len f)) in ( rng ( Line (G,( len G)))) & f is_sequence_on G implies (for i st 1 <= i & i <= ( len G) holds ex k st k in ( dom f) & (f /. k) in ( rng ( Line (G,i)))) & (for i st 1 <= i & i <= ( len G) & 2 <= ( len f) holds ( L~ f) meets ( rng ( Line (G,i)))) & for i, j, k, m st 1 <= i & i <= ( len G) & 1 <= j & j <= ( len G) & k in ( dom f) & m in ( dom f) & (f /. k) in ( rng ( Line (G,i))) & (for n st n in ( dom f) & (f /. n) in ( rng ( Line (G,i))) holds n <= k) & k < m & (f /. m) in ( rng ( Line (G,j))) holds i < j

    proof

      assume that

       A1: 1 <= ( len f) and

       A2: (f /. 1) in ( rng ( Line (G,1))) and

       A3: (f /. ( len f)) in ( rng ( Line (G,( len G)))) and

       A4: f is_sequence_on G;

      

       A5: ( len f) in ( dom f) by A1, FINSEQ_3: 25;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( len G) implies ex k st k in ( dom f) & (f /. k) in ( rng ( Line (G,$1)));

      

       A6: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A7: 1 <= k & k <= ( len G) implies ex i st i in ( dom f) & (f /. i) in ( rng ( Line (G,k)));

        assume that

         A8: 1 <= (k + 1) and

         A9: (k + 1) <= ( len G);

        

         A10: (k + 1) in ( dom G) by A8, A9, FINSEQ_3: 25;

        per cases ;

          suppose

           A11: k = 0 ;

          take 1;

          thus thesis by A1, A2, A11, FINSEQ_3: 25;

        end;

          suppose

           A12: k <> 0 ;

          defpred R[ Nat] means $1 in ( dom f) & (f /. $1) in ( rng ( Line (G,k)));

          

           A13: for i be Nat holds R[i] implies i <= ( len f) by FINSEQ_3: 25;

          

           A14: ( 0 + 1) <= k by A12, NAT_1: 13;

          then

           A15: ex i be Nat st R[i] by A7, A9, NAT_1: 13;

          consider m be Nat such that

           A16: R[m] & for i be Nat st R[i] holds i <= m from NAT_1:sch 6( A13, A15);

          take (m + 1);

          k <= ( len G) by A9, NAT_1: 13;

          then

           A17: k in ( dom G) by A14, FINSEQ_3: 25;

          thus thesis by A1, A3, A4, A10, A17, A16, Th21;

        end;

      end;

      

       A18: P[ 0 ];

      thus

       A19: for i holds P[i] from NAT_1:sch 2( A18, A6);

      thus for i st 1 <= i & i <= ( len G) & 2 <= ( len f) holds ( L~ f) meets ( rng ( Line (G,i)))

      proof

        let i;

        assume that

         A20: 1 <= i & i <= ( len G) and

         A21: 2 <= ( len f);

        consider k such that

         A22: k in ( dom f) and

         A23: (f /. k) in ( rng ( Line (G,i))) by A19, A20;

        (f /. k) in ( L~ f) by A21, A22, Th1;

        then (( L~ f) /\ ( rng ( Line (G,i)))) <> {} by A23, XBOOLE_0:def 4;

        hence thesis;

      end;

      let m, k, i, j;

      assume that

       A24: 1 <= m and

       A25: m <= ( len G) and

       A26: 1 <= k & k <= ( len G) and

       A27: i in ( dom f) and

       A28: j in ( dom f) and

       A29: (f /. i) in ( rng ( Line (G,m))) and

       A30: for n st n in ( dom f) & (f /. n) in ( rng ( Line (G,m))) holds n <= i and

       A31: i < j and

       A32: (f /. j) in ( rng ( Line (G,k)));

      

       A33: i <= ( len f) & j <= ( len f) by A27, A28, FINSEQ_3: 25;

      per cases ;

        suppose m = ( len G);

        then ( len f) <= i by A3, A5, A30;

        hence thesis by A31, A33, XXREAL_0: 1;

      end;

        suppose m <> ( len G);

        then m < ( len G) by A25, XXREAL_0: 1;

        then 1 <= (m + 1) & (m + 1) <= ( len G) by NAT_1: 11, NAT_1: 13;

        then

         A34: (m + 1) in ( dom G) by FINSEQ_3: 25;

        reconsider l = (j - i) as Element of NAT by A31, INT_1: 5;

        defpred P[ set] means for n,l be Nat st n = $1 & n > 0 & (i + n) in ( dom f) & (f /. (i + n)) in ( rng ( Line (G,l))) & l in ( dom G) holds m < l;

        

         A35: k in ( dom G) by A26, FINSEQ_3: 25;

        m in ( dom G) by A24, A25, FINSEQ_3: 25;

        then

         A36: (f /. (i + 1)) in ( rng ( Line (G,(m + 1)))) by A1, A3, A4, A27, A29, A30, A34, Th21;

        

         A37: for o be Nat st P[o] holds P[(o + 1)]

        proof

          let o be Nat such that

           A38: P[o];

          let n,l be Nat such that

           A39: n = (o + 1) and

           A40: n > 0 and

           A41: (i + n) in ( dom f) and

           A42: (f /. (i + n)) in ( rng ( Line (G,l))) and

           A43: l in ( dom G);

          per cases ;

            suppose o = 0 ;

            then l = (m + 1) by A34, A36, A39, A42, A43, Th2;

            hence thesis by NAT_1: 13;

          end;

            suppose

             A44: o <> 0 ;

            1 <= i by A27, FINSEQ_3: 25;

            then

             A45: 1 <= (i + o) by NAT_1: 12;

            (i + n) <= ( len f) & (i + o) <= ((i + o) + 1) by A41, FINSEQ_3: 25, NAT_1: 12;

            then (i + o) <= ( len f) by A39, XXREAL_0: 2;

            then

             A46: (i + o) in ( dom f) by A45, FINSEQ_3: 25;

            then

            consider l1 be Nat such that

             A47: l1 in ( dom G) and

             A48: (f /. (i + o)) in ( rng ( Line (G,l1))) by A4, Th19;

            

             A49: m < l1 by A38, A44, A46, A47, A48;

            

             A50: (i + n) = ((i + o) + 1) by A39;

            per cases by A4, A41, A50, A46, A47, A48, Th20;

              suppose (f /. (i + n)) in ( rng ( Line (G,l1)));

              hence thesis by A42, A43, A47, A49, Th2;

            end;

              suppose for k st (f /. (i + n)) in ( rng ( Line (G,k))) & k in ( dom G) holds |.(l1 - k).| = 1;

              then |.(l1 - l).| = 1 by A42, A43;

              per cases by SEQM_3: 41;

                suppose l1 > l & l1 = (l + 1);

                then m <= l by A49, NAT_1: 13;

                per cases by XXREAL_0: 1;

                  suppose m = l;

                  then (i + n) <= i by A30, A41, A42;

                  then n <= (i - i) by XREAL_1: 19;

                  hence thesis by A40;

                end;

                  suppose m < l;

                  hence thesis;

                end;

              end;

                suppose l1 < l & l = (l1 + 1);

                hence thesis by A49, XXREAL_0: 2;

              end;

            end;

          end;

        end;

        

         A51: P[ 0 ];

        

         A52: for o be Nat holds P[o] from NAT_1:sch 2( A51, A37);

         0 < (j - i) & (i + l) = j by A31, XREAL_1: 50;

        hence thesis by A28, A32, A52, A35;

      end;

    end;

    theorem :: GOBOARD1:30

    

     Th23: f is_sequence_on G & i in ( dom f) implies ex n st n in ( Seg ( width G)) & (f /. i) in ( rng ( Col (G,n)))

    proof

      assume f is_sequence_on G & i in ( dom f);

      then

      consider n, m such that

       A1: [n, m] in ( Indices G) and

       A2: (f /. i) = (G * (n,m));

      set L = ( Col (G,m));

      take m;

      

       A3: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      hence m in ( Seg ( width G)) by A1, ZFMISC_1: 87;

      

       A4: n in ( dom G) by A1, A3, ZFMISC_1: 87;

      ( len L) = ( len G) by MATRIX_0:def 8;

      then

       A5: n in ( dom L) by A4, FINSEQ_3: 29;

      (L . n) = (f /. i) by A2, A4, MATRIX_0:def 8;

      hence thesis by A5, FUNCT_1:def 3;

    end;

    theorem :: GOBOARD1:31

    

     Th24: f is_sequence_on G & i in ( dom f) & (i + 1) in ( dom f) & n in ( Seg ( width G)) & (f /. i) in ( rng ( Col (G,n))) implies (f /. (i + 1)) in ( rng ( Col (G,n))) or for k st (f /. (i + 1)) in ( rng ( Col (G,k))) & k in ( Seg ( width G)) holds |.(n - k).| = 1

    proof

      assume that

       A1: f is_sequence_on G and

       A2: i in ( dom f) and

       A3: (i + 1) in ( dom f) and

       A4: n in ( Seg ( width G)) & (f /. i) in ( rng ( Col (G,n)));

      consider j1,j2 be Nat such that

       A5: [j1, j2] in ( Indices G) and

       A6: (f /. (i + 1)) = (G * (j1,j2)) by A1, A3;

      

       A7: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      then

       A8: j1 in ( dom G) by A5, ZFMISC_1: 87;

      

       A9: j2 in ( Seg ( width G)) by A5, A7, ZFMISC_1: 87;

      ( len ( Col (G,j2))) = ( len G) by MATRIX_0:def 8;

      then

       A10: j1 in ( dom ( Col (G,j2))) by A8, FINSEQ_3: 29;

      consider i1,i2 be Nat such that

       A11: [i1, i2] in ( Indices G) and

       A12: (f /. i) = (G * (i1,i2)) by A1, A2;

      

       A13: i1 in ( dom G) by A11, A7, ZFMISC_1: 87;

      ( len ( Col (G,i2))) = ( len G) by MATRIX_0:def 8;

      then

       A14: i1 in ( dom ( Col (G,i2))) by A13, FINSEQ_3: 29;

      (( Col (G,i2)) . i1) = (f /. i) by A12, A13, MATRIX_0:def 8;

      then

       A15: (f /. i) in ( rng ( Col (G,i2))) by A14, FUNCT_1:def 3;

      i2 in ( Seg ( width G)) by A11, A7, ZFMISC_1: 87;

      then i2 = n by A4, A15, Th3;

      then

       A16: ( |.(i1 - j1).| + |.(n - j2).|) = 1 by A1, A2, A3, A11, A12, A5, A6;

      

       A17: (( Col (G,j2)) . j1) = (f /. (i + 1)) by A6, A8, MATRIX_0:def 8;

      then

       A18: (f /. (i + 1)) in ( rng ( Col (G,j2))) by A10, FUNCT_1:def 3;

      now

        per cases by A16, SEQM_3: 42;

          suppose |.(i1 - j1).| = 1 & n = j2;

          hence thesis by A17, A10, FUNCT_1:def 3;

        end;

          suppose |.(n - j2).| = 1 & i1 = j1;

          hence thesis by A9, A18, Th3;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD1:32

    

     Th25: 1 <= ( len f) & (f /. ( len f)) in ( rng ( Col (G,( width G)))) & f is_sequence_on G & i in ( Seg ( width G)) & (i + 1) in ( Seg ( width G)) & m in ( dom f) & (f /. m) in ( rng ( Col (G,i))) & (for k st k in ( dom f) & (f /. k) in ( rng ( Col (G,i))) holds k <= m) implies (m + 1) in ( dom f) & (f /. (m + 1)) in ( rng ( Col (G,(i + 1))))

    proof

      assume that

       A1: 1 <= ( len f) and

       A2: (f /. ( len f)) in ( rng ( Col (G,( width G)))) and

       A3: f is_sequence_on G and

       A4: i in ( Seg ( width G)) and

       A5: (i + 1) in ( Seg ( width G)) and

       A6: m in ( dom f) and

       A7: (f /. m) in ( rng ( Col (G,i))) and

       A8: for k st k in ( dom f) & (f /. k) in ( rng ( Col (G,i))) holds k <= m;

      defpred P[ Nat, set] means $2 in ( Seg ( width G)) & for k st k = $2 holds (f /. $1) in ( rng ( Col (G,k)));

      

       A9: ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      

       A10: for n st n in ( dom f) holds ex k st k in ( Seg ( width G)) & (f /. n) in ( rng ( Col (G,k)))

      proof

        assume not thesis;

        then

        consider n such that

         A11: n in ( dom f) and

         A12: for k st k in ( Seg ( width G)) holds not (f /. n) in ( rng ( Col (G,k)));

        consider i, j such that

         A13: [i, j] in ( Indices G) and

         A14: (f /. n) = (G * (i,j)) by A3, A11;

        

         A15: [i, j] in [:( dom G), ( Seg ( width G)):] by A13, MATRIX_0:def 4;

        then j in ( Seg ( width G)) by ZFMISC_1: 87;

        then

         A16: not (f /. n) in ( rng ( Col (G,j))) by A12;

        

         A17: i in ( dom G) by A15, ZFMISC_1: 87;

        then i in ( Seg ( len ( Col (G,j)))) by A9, MATRIX_0:def 8;

        then

         A18: i in ( dom ( Col (G,j))) by FINSEQ_1:def 3;

        (( Col (G,j)) . i) = (G * (i,j)) by A17, MATRIX_0:def 8;

        hence contradiction by A14, A16, A18, FUNCT_1:def 3;

      end;

      

       A19: for n be Nat st n in ( Seg ( len f)) holds ex r be Element of REAL st P[n, r]

      proof

        let n be Nat;

        assume n in ( Seg ( len f));

        then n in ( dom f) by FINSEQ_1:def 3;

        then

        consider k such that

         A20: k in ( Seg ( width G)) and

         A21: (f /. n) in ( rng ( Col (G,k))) by A10;

        reconsider r = k as Element of REAL by XREAL_0:def 1;

        take r;

        thus r in ( Seg ( width G)) by A20;

        let m;

        assume m = r;

        hence thesis by A21;

      end;

      consider v such that

       A22: ( dom v) = ( Seg ( len f)) and

       A23: for n be Nat st n in ( Seg ( len f)) holds P[n, (v . n)] from FINSEQ_1:sch 5( A19);

      

       A24: ( dom f) = ( Seg ( len f)) by FINSEQ_1:def 3;

      

       A25: for k st k in ( dom v) & (v . k) = i holds k <= m

      proof

        let k;

        assume that

         A26: k in ( dom v) and

         A27: (v . k) = i;

        (f /. k) in ( rng ( Col (G,i))) by A22, A23, A26, A27;

        hence thesis by A8, A22, A24, A26;

      end;

      

       A28: ( rng v) c= ( Seg ( width G))

      proof

        let x be object;

        assume x in ( rng v);

        then ex y be Nat st y in ( dom v) & (v . y) = x by FINSEQ_2: 10;

        hence thesis by A22, A23;

      end;

      

       A29: ( len v) = ( len f) by A22, FINSEQ_1:def 3;

      

       A30: for k st 1 <= k & k <= (( len v) - 1) holds for r, s st r = (v . k) & s = (v . (k + 1)) holds |.(r - s).| = 1 or r = s

      proof

        let k;

        assume that

         A31: 1 <= k and

         A32: k <= (( len v) - 1);

        

         A33: (k + 1) <= ( len v) by A32, XREAL_1: 19;

        let r, s;

        assume that

         A34: r = (v . k) and

         A35: s = (v . (k + 1));

        1 <= (k + 1) by NAT_1: 11;

        then

         A36: (k + 1) in ( dom f) by A29, A33, FINSEQ_3: 25;

        then

         A37: s in ( rng v) by A22, A24, A35, FUNCT_1:def 3;

        then

         A38: s in ( Seg ( width G)) by A28;

        k <= (k + 1) by NAT_1: 11;

        then k <= ( len f) by A29, A33, XXREAL_0: 2;

        then

         A39: k in ( dom f) by A31, FINSEQ_3: 25;

        then

         A40: r in ( rng v) by A22, A24, A34, FUNCT_1:def 3;

        then r in ( Seg ( width G)) by A28;

        then

        reconsider n1 = r, n2 = s as Element of NAT by A38;

        set L1 = ( Col (G,n1)), L2 = ( Col (G,n2));

        (f /. k) in ( rng L1) by A23, A24, A39, A34;

        then

        consider x be Nat such that

         A41: x in ( dom L1) and

         A42: (L1 . x) = (f /. k) by FINSEQ_2: 10;

        

         A43: ( dom L1) = ( Seg ( len L1)) & ( len L1) = ( len G) by FINSEQ_1:def 3, MATRIX_0:def 8;

        then

         A44: (f /. k) = (G * (x,n1)) by A9, A41, A42, MATRIX_0:def 8;

        (f /. (k + 1)) in ( rng L2) by A23, A24, A36, A35;

        then

        consider y be Nat such that

         A45: y in ( dom L2) and

         A46: (L2 . y) = (f /. (k + 1)) by FINSEQ_2: 10;

        reconsider x, y as Element of NAT by ORDINAL1:def 12;

         [x, n1] in [:( dom G), ( Seg ( width G)):] by A9, A28, A40, A41, A43, ZFMISC_1: 87;

        then

         A47: [x, n1] in ( Indices G) by MATRIX_0:def 4;

        

         A48: ( dom L2) = ( Seg ( len L2)) & ( len L2) = ( len G) by FINSEQ_1:def 3, MATRIX_0:def 8;

        then [y, n2] in [:( dom G), ( Seg ( width G)):] by A9, A28, A37, A45, ZFMISC_1: 87;

        then

         A49: [y, n2] in ( Indices G) by MATRIX_0:def 4;

        (f /. (k + 1)) = (G * (y,n2)) by A9, A48, A45, A46, MATRIX_0:def 8;

        then ( |.(x - y).| + |.(n1 - n2).|) = 1 by A3, A39, A36, A44, A47, A49;

        hence thesis by SEQM_3: 42;

      end;

      

       A50: (v . m) = i

      proof

        

         A51: (v . m) in ( Seg ( width G)) by A6, A23, A24;

        then

        reconsider k = (v . m) as Element of NAT ;

        assume

         A52: (v . m) <> i;

        (f /. m) in ( rng ( Col (G,k))) by A6, A23, A24;

        hence contradiction by A4, A7, A52, A51, Th3;

      end;

      1 <= m & m <= ( len f) by A6, FINSEQ_3: 25;

      then 1 <= ( len f) by XXREAL_0: 2;

      then

       A53: ( len f) in ( dom f) by FINSEQ_3: 25;

      

       A54: (v . ( len v)) = ( width G)

      proof

         0 < ( width G) by MATRIX_0: 44;

        then ( 0 + 1) <= ( width G) by NAT_1: 13;

        then

         A55: ( width G) in ( Seg ( width G)) by FINSEQ_1: 1;

        

         A56: (v . ( len v)) in ( Seg ( width G)) by A23, A29, A24, A53;

        then

        reconsider k = (v . ( len v)) as Element of NAT ;

        assume

         A57: (v . ( len v)) <> ( width G);

        (f /. ( len f)) in ( rng ( Col (G,k))) by A23, A29, A24, A53;

        hence contradiction by A2, A57, A56, A55, Th3;

      end;

      

       A58: v <> {} by A1, A22;

      hence (m + 1) in ( dom f) by A4, A5, A6, A22, A24, A28, A54, A30, A50, A25, SEQM_3: 45;

      (m + 1) in ( dom v) & (v . (m + 1)) = (i + 1) by A4, A5, A6, A22, A24, A58, A28, A54, A30, A50, A25, SEQM_3: 45;

      hence thesis by A22, A23;

    end;

    theorem :: GOBOARD1:33

    

     Th26: 1 <= ( len f) & (f /. 1) in ( rng ( Col (G,1))) & (f /. ( len f)) in ( rng ( Col (G,( width G)))) & f is_sequence_on G implies (for i st 1 <= i & i <= ( width G) holds ex k st k in ( dom f) & (f /. k) in ( rng ( Col (G,i)))) & (for i st 1 <= i & i <= ( width G) & 2 <= ( len f) holds ( L~ f) meets ( rng ( Col (G,i)))) & for i, j, k, m st 1 <= i & i <= ( width G) & 1 <= j & j <= ( width G) & k in ( dom f) & m in ( dom f) & (f /. k) in ( rng ( Col (G,i))) & (for n st n in ( dom f) & (f /. n) in ( rng ( Col (G,i))) holds n <= k) & k < m & (f /. m) in ( rng ( Col (G,j))) holds i < j

    proof

      assume that

       A1: 1 <= ( len f) and

       A2: (f /. 1) in ( rng ( Col (G,1))) and

       A3: (f /. ( len f)) in ( rng ( Col (G,( width G)))) and

       A4: f is_sequence_on G;

      

       A5: ( len f) in ( dom f) by A1, FINSEQ_3: 25;

      defpred P[ Nat] means 1 <= $1 & $1 <= ( width G) implies ex k st k in ( dom f) & (f /. k) in ( rng ( Col (G,$1)));

      

       A6: for k st P[k] holds P[(k + 1)]

      proof

        let k;

        assume

         A7: 1 <= k & k <= ( width G) implies ex i st i in ( dom f) & (f /. i) in ( rng ( Col (G,k)));

        assume that

         A8: 1 <= (k + 1) and

         A9: (k + 1) <= ( width G);

        

         A10: (k + 1) in ( Seg ( width G)) by A8, A9, FINSEQ_1: 1;

        per cases ;

          suppose

           A11: k = 0 ;

          take 1;

          thus thesis by A1, A2, A11, FINSEQ_3: 25;

        end;

          suppose

           A12: k <> 0 ;

          defpred R[ Nat] means $1 in ( dom f) & (f /. $1) in ( rng ( Col (G,k)));

          

           A13: for i be Nat holds R[i] implies i <= ( len f) by FINSEQ_3: 25;

          

           A14: ( 0 + 1) <= k by A12, NAT_1: 13;

          then

           A15: ex i be Nat st R[i] by A7, A9, NAT_1: 13;

          consider m be Nat such that

           A16: R[m] & for i be Nat st R[i] holds i <= m from NAT_1:sch 6( A13, A15);

          take (m + 1);

          k <= ( width G) by A9, NAT_1: 13;

          then

           A17: k in ( Seg ( width G)) by A14, FINSEQ_1: 1;

          thus thesis by A1, A3, A4, A10, A17, A16, Th25;

        end;

      end;

      

       A18: P[ 0 ];

      thus

       A19: for i holds P[i] from NAT_1:sch 2( A18, A6);

      thus for i st 1 <= i & i <= ( width G) & 2 <= ( len f) holds ( L~ f) meets ( rng ( Col (G,i)))

      proof

        let i;

        assume that

         A20: 1 <= i & i <= ( width G) and

         A21: 2 <= ( len f);

        consider k such that

         A22: k in ( dom f) and

         A23: (f /. k) in ( rng ( Col (G,i))) by A19, A20;

        (f /. k) in ( L~ f) by A21, A22, Th1;

        then (( L~ f) /\ ( rng ( Col (G,i)))) <> {} by A23, XBOOLE_0:def 4;

        hence thesis;

      end;

      let m, k, i, j;

      assume that

       A24: 1 <= m and

       A25: m <= ( width G) and

       A26: 1 <= k & k <= ( width G) and

       A27: i in ( dom f) and

       A28: j in ( dom f) and

       A29: (f /. i) in ( rng ( Col (G,m))) and

       A30: for n st n in ( dom f) & (f /. n) in ( rng ( Col (G,m))) holds n <= i and

       A31: i < j and

       A32: (f /. j) in ( rng ( Col (G,k)));

      

       A33: i <= ( len f) & j <= ( len f) by A27, A28, FINSEQ_3: 25;

      now

        per cases ;

          case m = ( width G);

          then ( len f) <= i by A3, A5, A30;

          hence contradiction by A31, A33, XXREAL_0: 1;

        end;

          case m <> ( width G);

          then m < ( width G) by A25, XXREAL_0: 1;

          then 1 <= (m + 1) & (m + 1) <= ( width G) by NAT_1: 11, NAT_1: 13;

          then

           A34: (m + 1) in ( Seg ( width G)) by FINSEQ_1: 1;

          reconsider l = (j - i) as Element of NAT by A31, INT_1: 5;

          defpred P[ set] means for n,l be Nat st n = $1 & n > 0 & (i + n) in ( dom f) & (f /. (i + n)) in ( rng ( Col (G,l))) & l in ( Seg ( width G)) holds m < l;

          

           A35: k in ( Seg ( width G)) by A26, FINSEQ_1: 1;

          m in ( Seg ( width G)) by A24, A25, FINSEQ_1: 1;

          then

           A36: (f /. (i + 1)) in ( rng ( Col (G,(m + 1)))) by A1, A3, A4, A27, A29, A30, A34, Th25;

          

           A37: for o be Nat st P[o] holds P[(o + 1)]

          proof

            let o be Nat such that

             A38: P[o];

            let n,l be Nat such that

             A39: n = (o + 1) and

             A40: n > 0 and

             A41: (i + n) in ( dom f) and

             A42: (f /. (i + n)) in ( rng ( Col (G,l))) and

             A43: l in ( Seg ( width G));

            now

              per cases ;

                suppose o = 0 ;

                then l = (m + 1) by A34, A36, A39, A42, A43, Th3;

                hence thesis by NAT_1: 13;

              end;

                suppose

                 A44: o <> 0 ;

                1 <= i by A27, FINSEQ_3: 25;

                then

                 A45: 1 <= (i + o) by NAT_1: 12;

                (i + n) <= ( len f) & (i + o) <= ((i + o) + 1) by A41, FINSEQ_3: 25, NAT_1: 12;

                then (i + o) <= ( len f) by A39, XXREAL_0: 2;

                then

                 A46: (i + o) in ( dom f) by A45, FINSEQ_3: 25;

                then

                consider l1 be Nat such that

                 A47: l1 in ( Seg ( width G)) and

                 A48: (f /. (i + o)) in ( rng ( Col (G,l1))) by A4, Th23;

                

                 A49: m < l1 by A38, A44, A46, A47, A48;

                

                 A50: (i + n) = ((i + o) + 1) by A39;

                now

                  per cases by A4, A41, A50, A46, A47, A48, Th24;

                    suppose (f /. (i + n)) in ( rng ( Col (G,l1)));

                    hence thesis by A42, A43, A47, A49, Th3;

                  end;

                    suppose for k st (f /. (i + n)) in ( rng ( Col (G,k))) & k in ( Seg ( width G)) holds |.(l1 - k).| = 1;

                    then

                     A51: |.(l1 - l).| = 1 by A42, A43;

                    now

                      per cases by A51, SEQM_3: 41;

                        suppose l1 > l & l1 = (l + 1);

                        then

                         A52: m <= l by A49, NAT_1: 13;

                        now

                          per cases by A52, XXREAL_0: 1;

                            case m = l;

                            then (i + n) <= i by A30, A41, A42;

                            then n <= (i - i) by XREAL_1: 19;

                            hence contradiction by A40;

                          end;

                            case m < l;

                            hence thesis;

                          end;

                        end;

                        hence thesis;

                      end;

                        suppose l1 < l & l = (l1 + 1);

                        hence thesis by A49, XXREAL_0: 2;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          

           A53: P[ 0 ];

          

           A54: for o be Nat holds P[o] from NAT_1:sch 2( A53, A37);

           0 < (j - i) & (i + l) = j by A31, XREAL_1: 50;

          hence thesis by A28, A32, A54, A35;

        end;

      end;

      hence thesis;

    end;

    theorem :: GOBOARD1:34

    

     Th27: k in ( Seg ( width G)) & (f /. 1) in ( rng ( Col (G,1))) & f is_sequence_on G & (for i st i in ( dom f) & (f /. i) in ( rng ( Col (G,k))) holds n <= i) implies for i st i in ( dom f) & i <= n holds for m st m in ( Seg ( width G)) & (f /. i) in ( rng ( Col (G,m))) holds m <= k

    proof

      assume that

       A1: k in ( Seg ( width G)) and

       A2: (f /. 1) in ( rng ( Col (G,1))) and

       A3: f is_sequence_on G and

       A4: for i st i in ( dom f) & (f /. i) in ( rng ( Col (G,k))) holds n <= i;

      defpred P[ Nat] means $1 in ( dom f) & $1 <= n implies for m st m in ( Seg ( width G)) & (f /. $1) in ( rng ( Col (G,m))) holds m <= k;

      

       A5: ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

       0 < ( width G) by MATRIX_0: 44;

      then ( 0 + 1) <= ( width G) by NAT_1: 13;

      then

       A6: 1 in ( Seg ( width G)) by FINSEQ_1: 1;

      

       A7: 1 <= k by A1, FINSEQ_1: 1;

      

       A8: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A9: P[i];

        assume that

         A10: (i + 1) in ( dom f) and

         A11: (i + 1) <= n;

        let m such that

         A12: m in ( Seg ( width G)) & (f /. (i + 1)) in ( rng ( Col (G,m)));

        now

          per cases ;

            suppose i = 0 ;

            hence thesis by A2, A6, A7, A12, Th3;

          end;

            suppose

             A13: i <> 0 ;

            (i + 1) <= ( len f) by A10, FINSEQ_3: 25;

            then

             A14: i <= ( len f) by NAT_1: 13;

            

             A15: i < n by A11, NAT_1: 13;

            

             A16: ( 0 + 1) <= i by A13, NAT_1: 13;

            then

             A17: i in ( dom f) by A14, FINSEQ_3: 25;

            then

            consider i1,i2 be Nat such that

             A18: [i1, i2] in ( Indices G) and

             A19: (f /. i) = (G * (i1,i2)) by A3;

            

             A20: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

            then

             A21: i2 in ( Seg ( width G)) by A18, ZFMISC_1: 87;

            

             A22: ( dom ( Col (G,i2))) = ( Seg ( len ( Col (G,i2)))) & ( len ( Col (G,i2))) = ( len G) by FINSEQ_1:def 3, MATRIX_0:def 8;

            

             A23: i1 in ( dom G) by A18, A20, ZFMISC_1: 87;

            then (( Col (G,i2)) . i1) = (f /. i) by A19, MATRIX_0:def 8;

            then

             A24: (f /. i) in ( rng ( Col (G,i2))) by A5, A23, A22, FUNCT_1:def 3;

            then

             A25: i2 <= k by A9, A11, A16, A14, A21, FINSEQ_3: 25, NAT_1: 13;

            now

              per cases by A25, XXREAL_0: 1;

                case

                 A26: i2 < k;

                now

                  per cases by A3, A10, A17, A21, A24, Th24;

                    suppose (f /. (i + 1)) in ( rng ( Col (G,i2)));

                    hence thesis by A12, A21, A26, Th3;

                  end;

                    suppose for j st (f /. (i + 1)) in ( rng ( Col (G,j))) & j in ( Seg ( width G)) holds |.(i2 - j).| = 1;

                    then

                     A27: |.(i2 - m).| = 1 by A12;

                    now

                      per cases by A27, SEQM_3: 41;

                        suppose i2 > m & i2 = (m + 1);

                        hence thesis by A26, XXREAL_0: 2;

                      end;

                        suppose i2 < m & m = (i2 + 1);

                        hence thesis by A26, NAT_1: 13;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

                case i2 = k;

                hence contradiction by A4, A15, A17, A24;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A28: P[ 0 ] by FINSEQ_3: 25;

      thus for n holds P[n] from NAT_1:sch 2( A28, A8);

    end;

    theorem :: GOBOARD1:35

    f is_sequence_on G & (f /. 1) in ( rng ( Col (G,1))) & (f /. ( len f)) in ( rng ( Col (G,( width G)))) & ( width G) > 1 & 1 <= ( len f) implies ex g st (g /. 1) in ( rng ( Col (( DelCol (G,( width G))),1))) & (g /. ( len g)) in ( rng ( Col (( DelCol (G,( width G))),( width ( DelCol (G,( width G))))))) & 1 <= ( len g) & g is_sequence_on ( DelCol (G,( width G))) & ( rng g) c= ( rng f)

    proof

      set D = ( DelCol (G,( width G)));

      assume that

       A1: f is_sequence_on G and

       A2: (f /. 1) in ( rng ( Col (G,1))) and

       A3: (f /. ( len f)) in ( rng ( Col (G,( width G)))) and

       A4: ( width G) > 1 and

       A5: 1 <= ( len f);

      consider k such that

       A6: ( width G) = (k + 1) and

       A7: k > 0 by A4, SEQM_3: 43;

      

       A8: ( width G) in ( Seg ( width G)) by A4, FINSEQ_1: 1;

      

       A9: ( len D) = ( len G) by MATRIX_0:def 13;

      

       A10: ( 0 + 1) <= k by A7, NAT_1: 13;

      then 1 < ( width G) by A6, NAT_1: 13;

      then

       A11: ( Col (D,1)) = ( Col (G,1)) by A6, A7, A8, Th6;

      

       A12: ( dom G) = ( Seg ( len G)) by FINSEQ_1:def 3;

      defpred P[ Nat] means $1 in ( dom f) & (f /. $1) in ( rng ( Col (G,k)));

      k <= (k + 1) by NAT_1: 11;

      then ex m st P[m] by A1, A2, A3, A5, A6, A10, Th26;

      then

       A13: ex m be Nat st P[m];

      consider m be Nat such that

       A14: P[m] & for i be Nat st P[i] holds m <= i from NAT_1:sch 5( A13);

      

       A15: ( width D) = k by A6, A8, MATRIX_0: 63;

      then ( width D) < ( width G) by A6, NAT_1: 13;

      then

       A16: ( Col (D,( width D))) = ( Col (G,( width D))) by A6, A10, A8, A15, Th6;

      

       A17: ( dom D) = ( Seg ( len D)) by FINSEQ_1:def 3;

      

       A18: for i st P[i] holds m <= i by A14;

      reconsider m as Element of NAT by ORDINAL1:def 12;

      

       A19: 1 <= m by A14, FINSEQ_3: 25;

      then

       A20: 1 in ( Seg m) by FINSEQ_1: 1;

      

       A21: ( Indices G) = [:( dom G), ( Seg ( width G)):] by MATRIX_0:def 4;

      take t = (f | m);

      m <= ( len f) by A14, FINSEQ_3: 25;

      then

       A22: ( len t) = m by FINSEQ_1: 59;

      then ( len t) in ( Seg m) by A19, FINSEQ_1: 1;

      hence (t /. 1) in ( rng ( Col (D,1))) & (t /. ( len t)) in ( rng ( Col (D,( width D)))) & 1 <= ( len t) by A2, A14, A15, A11, A16, A22, A20, FINSEQ_1: 1, FINSEQ_4: 71;

      

       A23: ( dom t) = ( Seg ( len t)) by FINSEQ_1:def 3;

      

       A24: ( Indices D) = [:( dom D), ( Seg ( width D)):] by MATRIX_0:def 4;

       A25:

      now

        k <= (k + 1) by NAT_1: 11;

        then

         A26: k in ( Seg ( width G)) by A6, A10, FINSEQ_1: 1;

        let n;

        assume

         A27: n in ( dom t);

        then

         A28: n <= m by A22, FINSEQ_3: 25;

        

         A29: n in ( dom f) by A14, A22, A23, A27, FINSEQ_4: 71;

        then

        consider i, j such that

         A30: [i, j] in ( Indices G) and

         A31: (f /. n) = (G * (i,j)) by A1;

        

         A32: j in ( Seg ( width G)) by A21, A30, ZFMISC_1: 87;

        then

         A33: 1 <= j by FINSEQ_1: 1;

        take i, j;

        

         A34: ( len ( Col (G,j))) = ( len G) & ( dom ( Col (G,j))) = ( Seg ( len ( Col (G,j)))) by FINSEQ_1:def 3, MATRIX_0:def 8;

        

         A35: i in ( dom G) by A21, A30, ZFMISC_1: 87;

        then (( Col (G,j)) . i) = (G * (i,j)) by MATRIX_0:def 8;

        then (f /. n) in ( rng ( Col (G,j))) by A12, A31, A35, A34, FUNCT_1:def 3;

        then j <= k by A1, A2, A18, A29, A28, A32, A26, Th27;

        then

         A36: j in ( Seg k) by A33, FINSEQ_1: 1;

        hence [i, j] in ( Indices D) by A9, A12, A17, A15, A24, A35, ZFMISC_1: 87;

        

        thus (t /. n) = (G * (i,j)) by A14, A22, A23, A27, A31, FINSEQ_4: 71

        .= (D * (i,j)) by A6, A7, A35, A36, Th13;

      end;

      now

        let n;

        assume that

         A37: n in ( dom t) and

         A38: (n + 1) in ( dom t);

        

         A39: n in ( dom f) & (n + 1) in ( dom f) by A14, A22, A23, A37, A38, FINSEQ_4: 71;

        let i1,i2,j1,j2 be Nat;

        assume that

         A40: [i1, i2] in ( Indices D) and

         A41: [j1, j2] in ( Indices D) and

         A42: (t /. n) = (D * (i1,i2)) and

         A43: (t /. (n + 1)) = (D * (j1,j2));

        

         A44: i1 in ( dom D) & i2 in ( Seg k) by A15, A24, A40, ZFMISC_1: 87;

        

         A45: j1 in ( dom D) & j2 in ( Seg k) by A15, A24, A41, ZFMISC_1: 87;

        (t /. n) = (f /. n) by A14, A22, A23, A37, FINSEQ_4: 71;

        then

         A46: (f /. n) = (G * (i1,i2)) by A6, A7, A9, A12, A17, A42, A44, Th13;

        k <= (k + 1) by NAT_1: 11;

        then

         A47: ( Seg k) c= ( Seg ( width G)) by A6, FINSEQ_1: 5;

        then

         A48: [j1, j2] in ( Indices G) by A9, A21, A12, A17, A45, ZFMISC_1: 87;

        (t /. (n + 1)) = (f /. (n + 1)) by A14, A22, A23, A38, FINSEQ_4: 71;

        then

         A49: (f /. (n + 1)) = (G * (j1,j2)) by A6, A7, A9, A12, A17, A43, A45, Th13;

         [i1, i2] in ( Indices G) by A9, A21, A12, A17, A44, A47, ZFMISC_1: 87;

        hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A1, A39, A46, A49, A48;

      end;

      hence t is_sequence_on D by A25;

      t = (f | ( Seg m)) by FINSEQ_1:def 15;

      hence thesis by RELAT_1: 70;

    end;

    theorem :: GOBOARD1:36

    f is_sequence_on G & (( rng f) /\ ( rng ( Col (G,1)))) <> {} & (( rng f) /\ ( rng ( Col (G,( width G))))) <> {} implies ex g st ( rng g) c= ( rng f) & (g /. 1) in ( rng ( Col (G,1))) & (g /. ( len g)) in ( rng ( Col (G,( width G)))) & 1 <= ( len g) & g is_sequence_on G

    proof

      assume that

       A1: f is_sequence_on G and

       A2: (( rng f) /\ ( rng ( Col (G,1)))) <> {} and

       A3: (( rng f) /\ ( rng ( Col (G,( width G))))) <> {} ;

      set y = the Element of (( rng f) /\ ( rng ( Col (G,( width G)))));

      set x = the Element of (( rng f) /\ ( rng ( Col (G,1))));

      

       A4: x in ( rng ( Col (G,1))) & y in ( rng ( Col (G,( width G)))) by A2, A3, XBOOLE_0:def 4;

      y in ( rng f) by A3, XBOOLE_0:def 4;

      then

      consider m be Element of NAT such that

       A5: m in ( dom f) and

       A6: y = (f /. m) by PARTFUN2: 2;

      

       A7: 1 <= m by A5, FINSEQ_3: 25;

      

       A8: x in ( rng f) by A2, XBOOLE_0:def 4;

      then

      consider n be Element of NAT such that

       A9: n in ( dom f) and

       A10: x = (f /. n) by PARTFUN2: 2;

      reconsider x as Point of ( TOP-REAL 2) by A10;

      

       A11: 1 <= n by A9, FINSEQ_3: 25;

      per cases by XXREAL_0: 1;

        suppose

         A12: n = m;

        reconsider h = <*x*> as FinSequence of ( TOP-REAL 2);

        

         A13: ( len h) = 1 by FINSEQ_1: 39;

         A14:

        now

          let k;

          assume

           A15: k in ( Seg 1);

          then

           A16: k = 1 by FINSEQ_1: 2, TARSKI:def 1;

          k in ( dom h) by A15, FINSEQ_1:def 8;

          

          hence (h /. k) = (h . k) by PARTFUN1:def 6

          .= x by A16, FINSEQ_1: 40;

        end;

        

         A17: ( rng h) c= ( rng f)

        proof

          let z be object;

          assume z in ( rng h);

          then

          consider i be Element of NAT such that

           A18: i in ( dom h) and

           A19: z = (h /. i) by PARTFUN2: 2;

          i in ( Seg 1) by A18, FINSEQ_1:def 8;

          hence thesis by A8, A14, A19;

        end;

        reconsider h as FinSequence of ( TOP-REAL 2);

        take h;

        thus ( rng h) c= ( rng f) by A17;

        1 in ( Seg 1) by FINSEQ_1: 1;

        hence (h /. 1) in ( rng ( Col (G,1))) & (h /. ( len h)) in ( rng ( Col (G,( width G)))) by A10, A4, A6, A12, A13, A14;

        

         A20: ( dom h) = ( Seg ( len h)) by FINSEQ_1:def 3;

         A21:

        now

          let i;

          assume that

           A22: i in ( dom h) and

           A23: (i + 1) in ( dom h);

          i = 1 by A13, A20, A22, FINSEQ_1: 2, TARSKI:def 1;

          hence for i1,i2,j1,j2 be Nat st [i1, i2] in ( Indices G) & [j1, j2] in ( Indices G) & (h /. i) = (G * (i1,i2)) & (h /. (i + 1)) = (G * (j1,j2)) holds ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A13, A20, A23, FINSEQ_1: 2, TARSKI:def 1;

        end;

        now

          consider i1,i2 be Nat such that

           A24: [i1, i2] in ( Indices G) & (f /. n) = (G * (i1,i2)) by A1, A9;

          let i such that

           A25: i in ( dom h);

          take i1, i2;

          thus [i1, i2] in ( Indices G) & (h /. i) = (G * (i1,i2)) by A10, A13, A14, A20, A25, A24;

        end;

        hence thesis by A21, FINSEQ_1: 39;

      end;

        suppose

         A26: n > m;

        n <= (n + 1) by NAT_1: 11;

        then

        reconsider l = ((n + 1) - m) as Element of NAT by A26, INT_1: 5, XXREAL_0: 2;

        set f1 = (f | n);

        defpred P[ Nat, set] means for k st ($1 + k) = (n + 1) holds $2 = (f1 /. k);

        

         A27: n in ( Seg n) by A11, FINSEQ_1: 1;

         A28:

        now

          let i;

          assume i in ( Seg l);

          then

           A29: i <= l by FINSEQ_1: 1;

          l <= ((n + 1) - 0 ) by XREAL_1: 13;

          hence ((n + 1) - i) is Element of NAT by A29, INT_1: 5, XXREAL_0: 2;

        end;

        

         A30: for i be Nat st i in ( Seg l) holds ex p st P[i, p]

        proof

          let i be Nat;

          assume i in ( Seg l);

          then

          reconsider a = ((n + 1) - i) as Element of NAT by A28;

          take (f1 /. a);

          let k;

          assume (i + k) = (n + 1);

          hence thesis;

        end;

        consider g such that

         A31: ( len g) = l & for i be Nat st i in ( Seg l) holds P[i, (g /. i)] from FINSEQ_4:sch 1( A30);

        take g;

        

         A32: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

        

         A33: for i st i in ( Seg l) holds ((n + 1) - i) is Element of NAT & (f1 /. ((n + 1) - i)) = (f /. ((n + 1) - i)) & ((n + 1) - i) in ( dom f)

        proof

          let i;

          assume

           A34: i in ( Seg l);

          then

           A35: i <= l by FINSEQ_1: 1;

          l <= ((n + 1) - 0 ) by XREAL_1: 13;

          then

          reconsider w = ((n + 1) - i) as Element of NAT by A35, INT_1: 5, XXREAL_0: 2;

          1 <= i by A34, FINSEQ_1: 1;

          then

           A36: ((n + 1) - i) <= ((n + 1) - 1) by XREAL_1: 13;

          ((n + 1) - l) <= ((n + 1) - i) by A35, XREAL_1: 13;

          then 1 <= ((n + 1) - i) by A7, XXREAL_0: 2;

          then w in ( Seg n) by A36, FINSEQ_1: 1;

          hence thesis by A9, FINSEQ_4: 71;

        end;

        thus ( rng g) c= ( rng f)

        proof

          let z be object;

          assume z in ( rng g);

          then

          consider i be Element of NAT such that

           A37: i in ( dom g) and

           A38: z = (g /. i) by PARTFUN2: 2;

          reconsider yy = ((n + 1) - i) as Element of NAT by A28, A31, A32, A37;

          (i + yy) = (n + 1);

          then

           A39: z = (f1 /. yy) by A31, A32, A37, A38;

          (f1 /. yy) = (f /. yy) & yy in ( dom f) by A33, A31, A32, A37;

          hence thesis by A39, PARTFUN2: 2;

        end;

        

         A40: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

         A41:

        now

          let i;

          assume that

           A42: i in ( dom g) and

           A43: (i + 1) in ( dom g);

          let i1,i2,j1,j2 be Nat;

          assume

           A44: [i1, i2] in ( Indices G) & [j1, j2] in ( Indices G) & (g /. i) = (G * (i1,i2)) & (g /. (i + 1)) = (G * (j1,j2));

          reconsider xx = ((n + 1) - (i + 1)) as Element of NAT by A28, A31, A40, A43;

          ((i + 1) + xx) = (n + 1);

          then (g /. (i + 1)) = (f1 /. xx) by A31, A32, A43;

          then

           A45: (g /. (i + 1)) = (f /. xx) by A33, A31, A32, A43;

          

           A46: (xx + 1) = ((n + 1) - i);

          reconsider ww = ((n + 1) - i) as Element of NAT by A28, A31, A40, A42;

          (i + ww) = (n + 1);

          then (g /. i) = (f1 /. ww) by A31, A32, A42;

          then

           A47: (g /. i) = (f /. ww) by A33, A31, A32, A42;

          ww in ( dom f) & xx in ( dom f) by A33, A31, A32, A42, A43;

          

          hence 1 = ( |.(j1 - i1).| + |.(j2 - i2).|) by A1, A47, A45, A46, A44

          .= ( |.( - (i1 - j1)).| + |.( - (i2 - j2)).|)

          .= ( |.(i1 - j1).| + |.( - (i2 - j2)).|) by COMPLEX1: 52

          .= ( |.(i1 - j1).| + |.(i2 - j2).|) by COMPLEX1: 52;

        end;

        (m + 1) <= n by A26, NAT_1: 13;

        then

         A48: (m + 1) <= (n + 1) by NAT_1: 13;

        then

         A49: 1 <= l by XREAL_1: 19;

        then 1 in ( Seg l) by FINSEQ_1: 1;

        

        then (g /. 1) = (f1 /. n) by A31

        .= (f /. n) by A9, A27, FINSEQ_4: 71;

        hence (g /. 1) in ( rng ( Col (G,1))) by A2, A10, XBOOLE_0:def 4;

        

         A50: m in ( Seg n) by A7, A26, FINSEQ_1: 1;

        reconsider ww = ((n + 1) - l) as Element of NAT ;

        

         A51: (l + ww) = (n + 1);

        ( len g) in ( dom g) by A31, A49, FINSEQ_3: 25;

        

        then (g /. ( len g)) = (f1 /. ww) by A31, A32, A51

        .= (f /. m) by A9, A50, FINSEQ_4: 71;

        hence (g /. ( len g)) in ( rng ( Col (G,( width G)))) by A3, A6, XBOOLE_0:def 4;

        now

          let i;

          assume

           A52: i in ( dom g);

          then

          reconsider ww = ((n + 1) - i) as Element of NAT by A28, A31, A40;

          ww in ( dom f) by A33, A31, A32, A52;

          then

          consider i1,i2 be Nat such that

           A53: [i1, i2] in ( Indices G) & (f /. ww) = (G * (i1,i2)) by A1;

          take i1, i2;

          (i + ww) = (n + 1);

          then (g /. i) = (f1 /. ww) by A31, A32, A52;

          hence [i1, i2] in ( Indices G) & (g /. i) = (G * (i1,i2)) by A33, A31, A32, A52, A53;

        end;

        hence thesis by A31, A48, A41, XREAL_1: 19;

      end;

        suppose

         A54: n < m;

        then

         A55: n in ( Seg m) by A11, FINSEQ_1: 1;

        m <= (m + 1) by NAT_1: 11;

        then

        reconsider l = ((m + 1) - n) as Element of NAT by A54, INT_1: 5, XXREAL_0: 2;

        reconsider w = (n - 1) as Element of NAT by A11, INT_1: 5;

        set f1 = (f | m);

        defpred P[ Nat, set] means $2 = (f1 /. (w + $1));

        

         A56: for i be Nat st i in ( Seg l) holds ex p st P[i, p];

        consider g such that

         A57: ( len g) = l & for i be Nat st i in ( Seg l) holds P[i, (g /. i)] from FINSEQ_4:sch 1( A56);

        reconsider ww = ((m + 1) - n) as Element of NAT by A57;

        

         A58: m in ( Seg m) by A7, FINSEQ_1: 1;

        take g;

        

         A59: ( dom g) = ( Seg l) by A57, FINSEQ_1:def 3;

        

         A60: for i st i in ( Seg l) holds (n - 1) is Element of NAT & (f1 /. (w + i)) = (f /. (w + i)) & ((n - 1) + i) in ( dom f)

        proof

          let i;

          assume

           A61: i in ( Seg l);

          then i <= l by FINSEQ_1: 1;

          then (i + n) <= (l + n) by XREAL_1: 7;

          then

           A62: ((i + n) - 1) <= m by XREAL_1: 20;

          1 <= i by A61, FINSEQ_1: 1;

          then ( 0 + 1) <= (w + i) by XREAL_1: 7;

          then (w + i) in ( Seg m) by A62, FINSEQ_1: 1;

          hence thesis by A5, FINSEQ_4: 71;

        end;

         A63:

        now

          let i;

          assume that

           A64: i in ( dom g) and

           A65: (i + 1) in ( dom g);

          (g /. i) = (f1 /. (w + i)) by A57, A59, A64;

          then

           A66: (g /. i) = (f /. (w + i)) by A60, A59, A64;

          (g /. (i + 1)) = (f1 /. (w + (i + 1))) by A57, A59, A65;

          then

           A67: ((w + i) + 1) in ( dom f) & (g /. (i + 1)) = (f /. ((w + i) + 1)) by A60, A59, A65;

          let i1,i2,j1,j2 be Nat;

          assume

           A68: [i1, i2] in ( Indices G) & [j1, j2] in ( Indices G) & (g /. i) = (G * (i1,i2)) & (g /. (i + 1)) = (G * (j1,j2));

          (w + i) in ( dom f) by A60, A59, A64;

          hence ( |.(i1 - j1).| + |.(i2 - j2).|) = 1 by A1, A66, A67, A68;

        end;

        

         A69: ( dom g) = ( Seg ( len g)) by FINSEQ_1:def 3;

        thus ( rng g) c= ( rng f)

        proof

          let z be object;

          assume z in ( rng g);

          then

          consider i be Element of NAT such that

           A70: i in ( dom g) and

           A71: z = (g /. i) by PARTFUN2: 2;

          

           A72: (w + i) in ( dom f) by A60, A57, A69, A70;

          z = (f1 /. (w + i)) & (f1 /. (w + i)) = (f /. (w + i)) by A60, A57, A69, A70, A71;

          hence thesis by A72, PARTFUN2: 2;

        end;

        (n + 1) <= m by A54, NAT_1: 13;

        then

         A73: (n + 1) <= (m + 1) by NAT_1: 13;

        then

         A74: 1 <= l by XREAL_1: 19;

        then 1 in ( Seg l) by FINSEQ_1: 1;

        

        then (g /. 1) = (f1 /. ((n - 1) + 1)) by A57

        .= (f /. n) by A5, A55, FINSEQ_4: 71;

        hence (g /. 1) in ( rng ( Col (G,1))) by A2, A10, XBOOLE_0:def 4;

        ( len g) in ( dom g) by A57, A74, FINSEQ_3: 25;

        

        then (g /. ( len g)) = (f1 /. (w + ww)) by A57, A59

        .= (f /. m) by A5, A58, FINSEQ_4: 71;

        hence (g /. ( len g)) in ( rng ( Col (G,( width G)))) by A3, A6, XBOOLE_0:def 4;

        now

          let i;

          assume

           A75: i in ( dom g);

          then (w + i) in ( dom f) by A60, A59;

          then

          consider i1,i2 be Nat such that

           A76: [i1, i2] in ( Indices G) & (f /. (w + i)) = (G * (i1,i2)) by A1;

          take i1, i2;

          (g /. i) = (f1 /. (w + i)) by A57, A59, A75;

          hence [i1, i2] in ( Indices G) & (g /. i) = (G * (i1,i2)) by A60, A59, A75, A76;

        end;

        hence thesis by A57, A73, A63, XREAL_1: 19;

      end;

    end;

    theorem :: GOBOARD1:37

    k in ( dom G) & f is_sequence_on G & (f /. ( len f)) in ( rng ( Line (G,( len G)))) & n in ( dom f) & (f /. n) in ( rng ( Line (G,k))) implies (for i st k <= i & i <= ( len G) holds ex j st j in ( dom f) & n <= j & (f /. j) in ( rng ( Line (G,i)))) & for i st k < i & i <= ( len G) holds ex j st j in ( dom f) & n < j & (f /. j) in ( rng ( Line (G,i)))

    proof

      assume that

       A1: k in ( dom G) and

       A2: f is_sequence_on G & (f /. ( len f)) in ( rng ( Line (G,( len G)))) and

       A3: n in ( dom f) and

       A4: (f /. n) in ( rng ( Line (G,k)));

      defpred P[ Nat] means k <= $1 & $1 <= ( len G) implies ex j st j in ( dom f) & n <= j & (f /. j) in ( rng ( Line (G,$1)));

      

       A5: 1 <= k by A1, FINSEQ_3: 25;

      

       A6: 1 <= n & n <= ( len f) by A3, FINSEQ_3: 25;

      

       A7: for i st P[i] holds P[(i + 1)]

      proof

        let i such that

         A8: P[i];

        assume that

         A9: k <= (i + 1) and

         A10: (i + 1) <= ( len G);

        per cases by A9, XXREAL_0: 1;

          suppose

           A11: k = (i + 1);

          take j = n;

          thus j in ( dom f) & n <= j & (f /. j) in ( rng ( Line (G,(i + 1)))) by A3, A4, A11;

        end;

          suppose

           A12: k < (i + 1);

          then k <= i by NAT_1: 13;

          then

           A13: 1 <= i by A5, XXREAL_0: 2;

          i <= ( len G) by A10, NAT_1: 13;

          then

           A14: i in ( dom G) by A13, FINSEQ_3: 25;

          1 <= (i + 1) by A5, A12, XXREAL_0: 2;

          then

           A15: (i + 1) in ( dom G) by A10, FINSEQ_3: 25;

          defpred P[ Nat] means $1 in ( dom f) & n <= $1 & (f /. $1) in ( rng ( Line (G,i)));

          

           A16: for j be Nat st P[j] holds j <= ( len f) by FINSEQ_3: 25;

          

           A17: ex j be Nat st P[j] by A8, A10, A12, NAT_1: 13;

          consider ma be Nat such that

           A18: P[ma] & for j be Nat st P[j] holds j <= ma from NAT_1:sch 6( A16, A17);

           A19:

          now

            let j such that

             A20: j in ( dom f) & (f /. j) in ( rng ( Line (G,i)));

            now

              per cases ;

                suppose j < n;

                hence j <= ma by A18, XXREAL_0: 2;

              end;

                suppose n <= j;

                hence j <= ma by A18, A20;

              end;

            end;

            hence j <= ma;

          end;

          take j = (ma + 1);

          

           A21: 1 <= ( len f) by A6, XXREAL_0: 2;

          hence j in ( dom f) by A2, A14, A15, A18, A19, Th21;

          ma <= (ma + 1) by NAT_1: 11;

          hence n <= j & (f /. j) in ( rng ( Line (G,(i + 1)))) by A2, A14, A15, A18, A21, A19, Th21, XXREAL_0: 2;

        end;

      end;

      

       A22: P[ 0 ] by A1, FINSEQ_3: 25;

      thus

       A23: for i holds P[i] from NAT_1:sch 2( A22, A7);

      let i;

      assume that

       A24: k < i and

       A25: i <= ( len G);

      consider j such that

       A26: j in ( dom f) and

       A27: n <= j and

       A28: (f /. j) in ( rng ( Line (G,i))) by A23, A24, A25;

      take j;

      thus j in ( dom f) by A26;

      1 <= i by A5, A24, XXREAL_0: 2;

      then i in ( dom G) by A25, FINSEQ_3: 25;

      then n <> j by A1, A4, A24, A28, Th2;

      hence thesis by A27, A28, XXREAL_0: 1;

    end;