The Mizar article:

Introduction to Go-Board --- Part I

by
Jaroslaw Kotowicz, and
Yatsuka Nakamura

Received August 24, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: GOBOARD1
[ MML identifier index ]


environ

 vocabulary PRE_TOPC, EUCLID, FINSEQ_1, ABSVALUE, ARYTM_1, FINSEQ_4, FUNCT_1,
      RELAT_1, BOOLE, FINSET_1, CARD_1, FINSEQ_2, MATRIX_2, ORDINAL2, SEQM_3,
      MCART_1, TOPREAL1, MATRIX_1, TREES_1, INCSP_1, GOBOARD1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, REAL_1, NUMBERS, XREAL_0,
      NAT_1, RELAT_1, FUNCT_1, CARD_1, FINSEQ_1, FINSET_1, SEQM_3, STRUCT_0,
      PRE_TOPC, ABSVALUE, FINSEQ_2, FINSEQ_4, EUCLID, TOPREAL1, MATRIX_1,
      MATRIX_2;
 constructors REAL_1, NAT_1, SEQM_3, ABSVALUE, TOPREAL1, MATRIX_2, FINSEQ_4,
      INT_1, MEMBERED, PARTFUN1, XBOOLE_0;
 clusters FINSET_1, RELSET_1, STRUCT_0, EUCLID, XREAL_0, FINSEQ_1, INT_1,
      RELAT_1, TOPREAL1, MEMBERED, ZFMISC_1, XBOOLE_0, NUMBERS, ORDINAL2;
 requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, MATRIX_1, SEQM_3, XBOOLE_0;
 theorems AXIOMS, TARSKI, REAL_1, NAT_1, ZFMISC_1, FUNCT_1, FINSEQ_1, ABSVALUE,
      SQUARE_1, FINSEQ_2, CARD_2, FINSEQ_3, REAL_2, MATRIX_1, TOPREAL1,
      MATRIX_2, TOPREAL3, FINSEQ_4, SEQM_3, PROB_1, RELAT_1, GROUP_5, INT_1,
      CARD_1, RLVECT_1, PARTFUN2, XBOOLE_0, XBOOLE_1, XCMPLX_1;
 schemes NAT_1, COMPTS_1, MATRIX_1, MATRIX_2;

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;

:::::::::::::::::::::::::::::
:: Real numbers preliminaries
:::::::::::::::::::::::::::::

theorem Th1:
abs(r-s)=1 iff r>s & r=s+1 or r<s & s=r+1
 proof
  thus abs(r-s)=1 implies r>s & r=s+1 or r<s & s=r+1
   proof assume
    A1: abs(r-s) = 1;
       now per cases by AXIOMS:21;
     case A2: r>s;
      then 0<r-s by SQUARE_1:11;
      then r-s=1 by A1,ABSVALUE:def 1;
      hence r>s & r=s+1 or r<s & s=r+1 by A2,XCMPLX_1:27;
     case r=s;
      then 1=abs(0) by A1,XCMPLX_1:14
      .= 0 by ABSVALUE:7;
      hence contradiction;
     case A3: r<s;
      then A4: 0<s-r by SQUARE_1:11;
        1=abs(-(r-s)) by A1,ABSVALUE:17
      .=abs(s-r) by XCMPLX_1:143
      .=s-r by A4,ABSVALUE:def 1;
      hence r>s & r=s+1 or r<s & s=r+1 by A3,XCMPLX_1:27;
     end;
    hence thesis;
   end;
  assume A5: r>s & r=s+1 or r<s & s=r+1;
   per cases by A5;
   suppose A6: r>s & r=s+1;
    then 0<r-s by SQUARE_1:11;
    hence abs(r-s)=r-s by ABSVALUE:def 1
    .= 1 by A6,XCMPLX_1:26;
   suppose A7: s>r & s=r+1;
    then A8: 0<s-r by SQUARE_1:11;
    thus abs(r-s)=abs(-(r-s)) by ABSVALUE:17
    .= abs(s-r) by XCMPLX_1:143
    .= s-r by A8,ABSVALUE:def 1
    .= 1 by A7,XCMPLX_1:26;
 end;

theorem Th2:
abs(i-j)+abs(n-m)=1 iff abs(i-j)=1 & n=m or abs(n-m)=1 & i=j
 proof
  thus abs(i-j)+abs(n-m)=1 implies abs(i-j)=1 & n=m or abs(n-m)=1 & i=j
   proof assume
    A1: abs(i-j)+abs(n-m)=1;
       now per cases;
     suppose A2: n=m;
      then 1=abs(i-j)+abs(0) by A1,XCMPLX_1:14
      .=abs(i-j)+0 by ABSVALUE:7
      .= abs(i-j);
      hence thesis by A2;
     suppose A3: n<>m;
         now per cases by A3,REAL_1:def 5;
       suppose A4: n<m;
        then reconsider l=m-n as Nat by INT_1:18;
          0<l & abs(-(m-n))=abs(l) by A4,ABSVALUE:17,SQUARE_1:11;
        then A5: 0+1<=l & abs(l)=l & 0<=abs(i-j) & abs(n-m)=abs(l)
         by ABSVALUE:5,def 1,NAT_1:38,XCMPLX_1:143;
then A6:        l<=1 by A1,REAL_2:173;
         then l=1 by A5,AXIOMS:21;
        then abs(i-j)=0 by A1,A5,XCMPLX_1:3;
        then i-j=0 by ABSVALUE:7;
        hence thesis by A5,A6,AXIOMS:21,XCMPLX_1:15;
       suppose A7: n>m;
        then reconsider l=n-m as Nat by INT_1:18;
          0<l by A7,SQUARE_1:11;
        then A8: 0+1<=l & abs(n-m)=l & 0<=abs(i-j)by ABSVALUE:5,def 1,NAT_1:38;
then A9:        l<=1 by A1,REAL_2:173;
         then l=1 by A8,AXIOMS:21;
        then abs(i-j)=0 by A1,A8,XCMPLX_1:3;
        then i-j=0 by ABSVALUE:7;
        hence thesis by A8,A9,AXIOMS:21,XCMPLX_1:15;
       end;
      hence thesis;
     end;
    hence thesis;
   end;
  assume A10: abs(i-j)=1 & n=m or abs(n-m)=1 & i=j;
     now per cases by A10;
   suppose A11: abs(i-j)=1 & n=m;
    then n-m=0 by XCMPLX_1:14;
    then abs(n-m)=0 by ABSVALUE:7;
    hence abs(i-j)+abs(n-m)=1 by A11;
   suppose A12: abs(n-m)=1 & i=j;
    then i-j=0 by XCMPLX_1:14;
    then abs(i-j)=0 by ABSVALUE:7;
    hence abs(i-j)+abs(n-m)=1 by A12;
   end;
  hence thesis;
 end;

theorem Th3:
n>1 iff ex m st n=m+1 & m>0
 proof
  thus n>1 implies ex m st n=m+1 & m>0
   proof assume
    A1: 1<n;
    then 0<>n; then consider m such that
    A2: n = m+1 by NAT_1:22;
    take m;
       m <> 0 by A1,A2;
    hence thesis by A2,NAT_1:19;
   end;
  given m such that
  A3: n=m+1 & m>0;
    0+1<n by A3,REAL_1:53;
  hence thesis;
 end;

begin :: Finite sequences preliminaries

scheme FinSeqDChoice{D()->non empty set, N()->Nat, P[set,set]}:
 ex f being FinSequence of D() st
   len f = N() & for n st n in Seg N() holds P[n,f/.n]
provided
A1: for n st n in Seg N() ex d being Element of D() st P[n,d]
  proof
   reconsider X=D() as set;
   defpred P1[set,set] means P[$1,$2] & $2 in D();
   A2: now let x be set; assume
        A3: x in Seg N();
        then reconsider x'=x as Nat;
        consider d be Element of D() such that
        A4: P[x',d] by A1,A3;
        reconsider y=d as set;
        take y;
        thus y in X & P1[x,y] by A4;
       end;
   consider f be Function such that
   A5: dom f = Seg N() & rng f c= X &
       for x be set st x in Seg N() holds P1[x,f.x]
       from NonUniqBoundFuncEx(A2);
   reconsider f as FinSequence by A5,FINSEQ_1:def 2;
   reconsider f as FinSequence of D() by A5,FINSEQ_1:def 4;
   take f;
   thus
   len f = N() by A5,FINSEQ_1:def 3;
   let n; assume
A6:  n in Seg N();
then P[n,f.n] by A5;
   hence P[n,f/.n] by A5,A6,FINSEQ_4:def 4;
  end;

theorem Th4:
n = m + 1 & i in Seg n implies len Sgm(Seg n \ {i}) = m
 proof assume
  A1: n = m + 1 & i in Seg n;
  set X = Seg n \ {i};
  A2: X c= Seg n & i in {i} by TARSKI:def 1,XBOOLE_1:36;
   then not i in X & Seg n is finite by XBOOLE_0:def 4;
  then card X + 1 = card (X \/ {i}) by CARD_2:54
   .= card ((Seg n) \/ {i}) by XBOOLE_1:39
   .= card (Seg n) by A1,ZFMISC_1:46
   .= m + 1 by A1,FINSEQ_1:78;
  then card X = m by XCMPLX_1:2;
  hence thesis by A2,FINSEQ_3:44;
 end;

theorem Th5:
n=m+1 & k in Seg n & i in Seg m implies (1<=i & i<k implies
 Sgm(Seg n \ {k}).i = i) &
 (k<=i & i<=m implies Sgm(Seg n \ {k}).i = i+1)
 proof
  defpred P[Nat] means
   for n,k,i st n = $1 + 1 & k in Seg n & i in Seg $1 holds
          (1<=i & i<k implies Sgm(Seg n \ {k}).i = i) &
          (k<=i & i<=$1implies Sgm(Seg n \ {k}).i = i+1);
  A1: P[0] by FINSEQ_1:4;
  A2: for k st P[k] holds P[k+1]
   proof let k such that
    A3: P[k];
    let g,i,n be Nat; assume that
    A4: g = k+1 + 1 and
    A5: i in Seg g and
    A6: n in Seg(k+1);
    set X = Seg g \ {i};
    A7: X c= Seg g by XBOOLE_1:36;
    then A8: rng Sgm(X) = X by FINSEQ_1:def 13;
    A9: len Sgm(X)=k+1 by A4,A5,Th4;
    A10: 1<=i & i<=g & 1<=n & n<=k+1 by A5,A6,FINSEQ_1:3;
       now per cases;
     suppose A11: i=g;
      then A12: k+1<i by A4,NAT_1:38;
        X = Seg(k+1)
       proof
        thus X c= Seg(k+1)
         proof let x; assume x in X;
          then A13: x in Seg g & not x in {i} & Seg g = {j: 1<=j & j<=g}
               by FINSEQ_1:def 1,XBOOLE_0:def 4; then consider j such that
          A14: x=j & 1<=j & j<=g;
            x<>i by A13,TARSKI:def 1;
          then j<g by A11,A14,REAL_1:def 5;
          then j<=k+1 by A4,NAT_1:38;
          hence thesis by A14,FINSEQ_1:3;
         end;
        let x; assume x in Seg(k+1);
        then x in {j: 1<=j & j<=k+1} by FINSEQ_1:def 1; then consider j such
that
        A15: x=j & 1<=j & j<=k+1;
          k+1<=g by A4,NAT_1:29;
        then j<=g by A15,AXIOMS:22;
        then A16: j in Seg g by A15,FINSEQ_1:3;
          not j in {i} by A12,A15,TARSKI:def 1;
        hence thesis by A15,A16,XBOOLE_0:def 4;
       end;
      then A17: Sgm X = idseq (k+1) by FINSEQ_3:54;
      thus 1<=n & n<i implies Sgm(X).n = n
       proof assume 1<=n & n<i;
          idseq(k+1)=id Seg(k+1) by FINSEQ_2:def 1;
        hence (Sgm X).n = n by A6,A17,FUNCT_1:34;
       end;
      thus i<=n & n<=k+1 implies Sgm(Seg g \ {i}).n = n+1 by A4,A11,NAT_1:38;
     suppose A18: i<>g;
then A19:      i<g by A10,REAL_1:def 5;
      then A20: i<=k+1 by A4,NAT_1:38;
        1<=k+1 by A10,AXIOMS:22;
      then k+1 in dom Sgm(X) by A9,FINSEQ_3:27;
      then A21: Sgm(X).(k+1) in X by A8,FUNCT_1:def 5;
      set A = {l where l is Nat : 1<=l & l<=g & l<>i};
      A22: X = A
       proof
        thus X c= A
         proof let x; assume x in X;
          then A23: x in Seg g & not x in {i} & Seg g= {j: 1<=j & j<=g}
                by FINSEQ_1:def 1,XBOOLE_0:def 4; then consider m such that
          A24: x=m & 1<=m & m<=g;
            m<>i by A23,A24,TARSKI:def 1;
          hence x in A by A24;
         end;
        let x; assume x in A; then consider m such that
        A25: x=m & 1<=m & m<=g & m<>i;
          m in Seg g & not m in {i} by A25,FINSEQ_1:3,TARSKI:def 1;
        hence thesis by A25,XBOOLE_0:def 4;
       end;
then A26:      ex j st Sgm(X).(k+1) = j & 1<=j & j<=g & j<>i by A21;
        1<=g & g<=g & g<>i by A10,A18,AXIOMS:22;
      then g in rng Sgm(X) by A8,A22;
      then consider x be Nat such that
      A27: x in dom Sgm(X) & Sgm(X).x=g by FINSEQ_2:11;
      A28: 1<=x & x<=k+1 & k+1<=len Sgm(X) by A9,A27,FINSEQ_3:27;
then A29:      k+1<=x by A7,A26,A27,FINSEQ_1:def 13;
         now per cases by A10,REAL_1:def 5;
       suppose A30: n=k+1;
        hence 1<=n & n<i implies Sgm(X).n = n by A4,A19,NAT_1:38;
        thus i<=n & n<=k+1 implies Sgm(Seg g \ {i}).n=n+1 by A4,A27,A28,A29,A30
,AXIOMS:21;
       suppose A31: n<k+1;
         then n<=k by NAT_1:38;
        then A32: n in Seg k & i in Seg(k+1) by A10,A20,FINSEQ_1:3;
        then A33: (1<=n & n<i implies Sgm(Seg(k+1) \ {i}).n = n) &
            (i<=n & n<=k implies Sgm(Seg(k+1) \ {i}).n = n+1) by A3;
        set Y = Seg(k+1) \ {i};
        A34: X = Y \/ {g}
         proof
          thus X c= Y \/ {g}
           proof let x; assume x in X; then consider j such that
            A35: x=j & 1<=j & j<=g & j<>i by A22;
               now per cases by A35,REAL_1:def 5;
             suppose j=g;
              then x in {g} by A35,TARSKI:def 1;
              hence thesis by XBOOLE_0:def 2;
             suppose j<g; then j<=k+1 by A4,NAT_1:38;
              then j in Seg(k+1) & not j in {i} by A35,FINSEQ_1:3,TARSKI:def 1
;
              then x in Y by A35,XBOOLE_0:def 4;
              hence thesis by XBOOLE_0:def 2;
             end;
            hence thesis;
           end;
          let x such that A36: x in Y \/ {g};
             now per cases by A36,XBOOLE_0:def 2;
           suppose x in Y;
            then A37: x in Seg(k+1) & not x in {i} &
            Seg(k+1)={ s where s is Nat :1<=s & s<=k+1}
             by FINSEQ_1:def 1,XBOOLE_0:def 4; then consider s be Nat such that
            A38: x=s & 1<=s & s<=k+1;
              k+1<=g by A4,NAT_1:29;
            then s<=g & s<>i by A37,A38,AXIOMS:22,TARSKI:def 1;
            hence x in X by A22,A38;
           suppose x in {g};
            then x=g & 1<=g by A10,AXIOMS:22,TARSKI:def 1;
            hence thesis by A18,A22;
           end;
          hence thesis;
         end;
        A39: now let j1,j be Nat; assume j1 in Y & j in {g};
          then A40: j1 in Seg(k+1) & j=g by TARSKI:def 1,XBOOLE_0:def 4;
          then j1<=k+1 by FINSEQ_1:3;
          hence j1<j by A4,A40,NAT_1:38;
         end;
          Y c=X & {g} c= X by A34,XBOOLE_1:7;
        then Y c= Seg g & {g} c= Seg g by A7,XBOOLE_1:1;
        then A41: Sgm(X) = Sgm(Y)^Sgm({g}) by A34,A39,FINSEQ_3:48;
        A42: len Sgm(Y) = k by A32,Th4;
           now assume
          A43: 1<=n & n<i;
            n in Seg len Sgm(Y) by A32,Th4;
          then n in dom Sgm(Y) by FINSEQ_1:def 3;
          hence Sgm(X).n = n by A33,A41,A43,FINSEQ_1:def 7;
         end;
        hence 1<=n & n<i implies Sgm(X).n = n;
        assume
        A44: i<=n & n<=k+1;
           n<=k by A31,NAT_1:38;
        then n in Seg k by A10,FINSEQ_1:3;
        then n in dom Sgm(Y) by A42,FINSEQ_1:def 3;
        hence Sgm(X).n = n+1 by A31,A33,A41,A44,FINSEQ_1:def 7,NAT_1:38;
       end;
      hence thesis;
     end;
    hence thesis;
   end;
  A45: for k holds P[k] from Ind(A1,A2);
  assume n = m + 1 & k in Seg n & i in Seg m;
  hence thesis by A45;
 end;

theorem Th6:
for f being FinSequence, n,m st len f = m+1 & n in dom f holds len Del(f,n)=m
 proof let f be FinSequence, n,m such that
  A1: len f = m+1 & n in dom f;
    ex k st len f = k+1 & len Del(f,n) = k by A1,MATRIX_2:8;
  hence thesis by A1,XCMPLX_1:2;
 end;

theorem Th7:
for f being FinSequence,n,m,k st len f = m+1 & n in dom f & k in Seg m holds
Del(f,n).k = f.k or Del(f,n).k = f.(k+1)
 proof let f be FinSequence,n,m,k such that
  A1: len f = m+1 & n in dom f & k in Seg m;
  set X = dom f \ {n};
  A2: dom f=Seg len f & dom Sgm(X)=Seg len Sgm(X) by FINSEQ_1:def 3;
  then A3: Del(f,n) = f*Sgm(X) & X c= Seg len f by MATRIX_2:def 5,XBOOLE_1:36;
  then rng Sgm(X) = X by FINSEQ_1:def 13;
  then A4: dom (f*Sgm(X)) = dom Sgm(X) & len Sgm(X) = m
   by A1,A2,A3,Th4,RELAT_1:46;
    (1<=k & k<n implies Sgm(X).k=k) & (n<=k & k<=m implies Sgm(X).k=k+1)
   by A1,A2,Th5;
    hence thesis by A1,A2,A3,A4,FINSEQ_3:27,FUNCT_1:22;
 end;

theorem Th8:
for f being FinSequence,n,m,k st len f = m+1 & k<n holds Del(f,n).k = f.k
 proof let f be FinSequence,n,m,k; assume
  A1: len f = m+1 & k<n;
  per cases;
  suppose A2: n in dom f;
    now per cases;
  suppose A3: 1 <= k;
    n<=m+1 by A1,A2,FINSEQ_3:27;
  then k<m+1 by A1,AXIOMS:22;
  then k<=m by NAT_1:38;
  then A4: k in Seg m by A3,FINSEQ_1:3;
  set X = dom f \ {n};
  A5: dom f=Seg len f & dom Sgm(X)=Seg len Sgm(X) by FINSEQ_1:def 3;
  then A6: Del(f,n) = f*Sgm(X) & X c= Seg len f by MATRIX_2:def 5,XBOOLE_1:36;
  then rng Sgm(X) = X by FINSEQ_1:def 13;
then A7: dom (f*Sgm(X)) = dom Sgm(X) & len Sgm(X) = m by A1,A2,A5,A6,Th4,
RELAT_1:46;
    1<=k & k<n implies Sgm(X).k = k by A1,A2,A4,A5,Th5;
  hence thesis by A1,A3,A4,A5,A6,A7,FUNCT_1:22;
  suppose A8:not 1 <= k;
then not k in dom f by FINSEQ_3:27;
then A9:f.k = {} by FUNCT_1:def 4;
    Seg len Del (f,n) = Seg m by A1,A2,Th6;
  then dom Del (f,n) = Seg m by FINSEQ_1:def 3;
  then not k in dom Del (f,n) by A8,FINSEQ_1:3;
  hence thesis by A9,FUNCT_1:def 4;
  end;
  hence thesis;
  suppose not n in dom f;
  hence thesis by MATRIX_2:8;
 end;

theorem Th9:
for f being FinSequence,n,m,k st len f = m+1 & n in dom f & n<=k & k<=m holds
Del(f,n).k = f.(k+1)
 proof let f be FinSequence,n,m,k; assume
  A1: len f = m+1 & n in dom f & n<=k & k<=m;
  then 1<=n by FINSEQ_3:27;
  then 1<=k by A1,AXIOMS:22;
  then A2: k in Seg m by A1,FINSEQ_1:3;
  set X = dom f \ {n};
  A3: dom f=Seg len f & dom Sgm(X)=Seg len Sgm(X) by FINSEQ_1:def 3;
  then A4: Del(f,n) = f*Sgm(X) & X c= Seg len f by MATRIX_2:def 5,XBOOLE_1:36;
  then rng Sgm(X) = X by FINSEQ_1:def 13;
  then A5: dom (f*Sgm(X)) = dom Sgm(X) & len Sgm(X) = m
   by A1,A3,A4,Th4,RELAT_1:46;
    n<=k & k<=m implies Sgm(X).k = k+1 by A1,A2,A3,Th5;
  hence thesis by A1,A2,A3,A4,A5,FUNCT_1:22;
 end;

theorem Th10:
for D being set, f being FinSequence of D, n,m
    st n in dom f & m in Seg n holds m in dom f & (f|n)/.m = f/.m
 proof let D be set, f be FinSequence of D, n,m; assume
  A1: n in dom f & m in Seg n;
  A2: dom f = Seg len f & f|n = f|Seg n by FINSEQ_1:def 3,TOPREAL1:def 1;
    n<=len f by A1,FINSEQ_3:27;
  then A3: Seg n c= dom f by A2,FINSEQ_1:7;
  hence
  m in dom f by A1;
A4: Seg n = dom f /\ Seg n by A3,XBOOLE_1:28
   .= dom(f|n) by A2,FUNCT_1:68;
  hence (f|n)/.m = (f|n).m by A1,FINSEQ_4:def 4
      .= f.m by A1,A2,A4,FUNCT_1:68
      .= f/.m by A1,A3,FINSEQ_4:def 4;
 end;

definition let f be FinSequence of REAL, k be Nat;
 redefine func f.k -> Real;
 coherence
  proof
   per cases;
   suppose k in dom f;
    then f.k = f/.k by FINSEQ_4:def 4;
   hence thesis;
   suppose not k in dom f;
   hence thesis by CARD_1:51,FUNCT_1:def 4;
  end;
end;

definition let IT be FinSequence of REAL;
 attr IT is increasing means :Def1:
  for n,m st n in dom IT & m in dom IT & n<m holds IT.n < IT.m;
end;

definition let f be FinSequence;
redefine attr f is constant means :Def2:
 for n,m st n in dom f & m in dom f holds f.n=f.m;
 compatibility
  proof
   thus f is constant implies
     for n,m st n in dom f & m in dom f holds f.n=f.m by SEQM_3:def 5;
   assume
A1: for n,m st n in dom f & m in dom f holds f.n=f.m;
   let n,m be set;
   assume n in dom f & m in dom f;
   hence thesis by A1;
  end;
end;

definition
cluster non empty increasing FinSequence of REAL;
 existence
  proof consider x being Real;
   take v = <*x*>;
A1:  dom<*x*> = { 1 } by FINSEQ_1:4,55;
   thus v is non empty by FINSEQ_1:4,55,RELAT_1:60;
   let n,m; assume n in dom v & m in dom v;
    then n = 1 & m = 1 by A1,TARSKI:def 1;
   hence thesis;
  end;
end;

definition let D be non empty set;
cluster non empty FinSequence of D;
 existence
  proof consider x being Element of D;
   take v = <*x*>;
  thus v is non empty by FINSEQ_1:4,55,RELAT_1:60;
  end;
end;

definition
cluster constant FinSequence of REAL;
 existence
  proof
   take v = <*>REAL;
   let n,m; assume
      n in dom v & m in dom v;
   hence thesis;
  end;
end;

definition let f;
func X_axis(f) -> FinSequence of REAL means :Def3:
 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 st k in Seg len f ex r st P[k,r];
    consider v such that
    A2: dom v = Seg len f and
    A3: for k st k in Seg len f holds P[k,v.k] from SeqDEx(A1);
    take v;
    thus len v = len f by A2,FINSEQ_1:def 3;
    let n; assume
       n in dom v;
    hence v.n = (f/.n)`1 by A2,A3;
   end;
  uniqueness
   proof let v1,v2; assume that
    A4: len v1 = len f & for n st n in dom v1 holds v1.n = (f/.n)`1
      and
    A5: len v2 = len f & for n st n in dom v2 holds v2.n = (f/.n)`1;
    A6: dom v1 = Seg len v1 & dom v2 = Seg len v2 & dom f = Seg len f
      by FINSEQ_1:def 3;
       now let n; assume
      A7: n in (dom f);
      hence v1.n = (f/.n)`1 by A4,A6
               .= v2.n by A5,A6,A7;
     end;
    hence thesis by A4,A5,A6,FINSEQ_1:17;
   end;
func Y_axis(f) -> FinSequence of REAL means :Def4:
 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;
    A8: for k st k in Seg len f ex r st P[k,r];
    consider v such that
    A9: dom v = Seg len f and
    A10: for k st k in Seg len f holds P[k,v.k] from SeqDEx(A8);
    take v;
    thus len v = len f by A9,FINSEQ_1:def 3;
    let n; assume
       n in dom v;
    hence v.n = (f/.n)`2 by A9,A10;
   end;
  uniqueness
   proof let v1,v2; assume that
    A11: len v1 = len f & for n st n in dom v1 holds v1.n = (f/.n)`2
      and
    A12: len v2 = len f & for n st n in dom v2 holds v2.n = (f/.n)`2;
    A13: dom v1 = Seg len v1 & dom v2 = Seg len v2 & dom f = Seg len f
      by FINSEQ_1:def 3;
       now let n; assume
      A14: n in (dom f);
      hence v1.n = (f/.n)`2 by A11,A13
               .= v2.n by A12,A13,A14;
     end;
    hence thesis by A11,A12,A13,FINSEQ_1:17;
   end;
end;

canceled 3;

theorem Th14:
v<>{} & rng v c= Seg n & v.(len v) = n &
(for k st 1<=k & k<=len v - 1 holds
  for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s) & i in Seg n &
i+1 in Seg n & m in dom v & v.m = i &
(for k st k in dom v & v.k = i holds k<=m) implies
m+1 in dom v & v.(m+1)=i+1
 proof assume that
  A1: v<>{} and
  A2: rng v c= Seg n and
  A3: v.(len v) = n and
  A4: for k st 1<=k & k<=len v - 1 holds
        for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s and
  A5: i in Seg n and
  A6: i+1 in Seg n and
  A7: m in dom v and
  A8: v.m = i and
  A9: for k st k in dom v & v.k = i holds k<=m;
    len v <> 0 by A1,FINSEQ_1:25;
  then 0 < len v by NAT_1:19;
  then 0+1<=len v & len v<=len v by NAT_1:38;
  then A10: len v in dom v by FINSEQ_3:27;
  A11: 1<=i & i<=n & 1<=i+1 & i+1<=n by A5,A6,FINSEQ_1:3;
  A12: 1<=m & m<=len v & m<=m+1 by A7,FINSEQ_3:27,NAT_1:29;
  A13: now assume not m+1 in dom v;
             then 1>m+1 or m+1>len v by FINSEQ_3:27;
            then len v <=m & i<n by A11,NAT_1:29,38;
            hence contradiction by A3,A8,A12,AXIOMS:21;
          end;
   reconsider r=v.(m+1) as Real;
     m+1<=len v by A13,FINSEQ_3:27;
   then A14: m<=len v - 1 & m<len v by NAT_1:38,REAL_1:84;
      now per cases by A4,A8,A12,A14;
    case A15: abs(i - r) = 1;
        now per cases by A15,Th1;
      case A16: i>r & i=r+1;
       defpred P[set] means
            for k,r st k=$1 & k>0 & m+k in dom v & r=v.(m+k) holds r<i;
       A17: P[0];
       A18: for k st P[k] holds P[k+1]
        proof let k such that
         A19: P[k];
         let j,s such that
         A20: j=k+1 & j>0 & m+j in dom v & s=v.(m+j);
            now per cases;
          suppose k=0;
           hence s<i by A16,A20;
          suppose k<>0;
           then A21: 0<k & m<=m+k & m+k<=m+k+1 & m+k+1 = m+(k+1)
            by NAT_1:19,29,XCMPLX_1:1;
           then A22: 1<=m+k & m+(k+1)<=len v by A12,A20,AXIOMS:22,FINSEQ_3:27;
           then 1<=m+k & m+k<=len v by A21,AXIOMS:22;
           then A23: m+k in dom v by FINSEQ_3:27;
           then v.(m+k) in rng v by FUNCT_1:def 5;
           then v.(m+k) in Seg n & Seg n c= NAT by A2;
           then reconsider r1=v.(m+k) as Nat;
           A24: r1<i by A19,A21,A23;
A25:           m+k<=len v - 1 by A21,A22,REAL_1:84;
              now per cases by A4,A20,A21,A22,A25;
            suppose A26: abs(r1-s)=1;
                now per cases by A26,Th1;
              suppose r1>s & r1=s+1; hence s<i by A24,AXIOMS:22;
              suppose r1<s & s=r1+1; then A27: s<=i by A24,NAT_1:38;
                  now per cases by A27,REAL_1:def 5;
                case s<i; hence thesis;
                case s=i; then m+j<=m by A9,A20;
                 then j<=m-m by REAL_1:84;
                 hence contradiction by A20,XCMPLX_1:14;
                end;
               hence thesis;
              end;
             hence thesis;
            suppose r1=s; hence thesis by A19,A21,A23;
            end;
           hence thesis;
          end;
         hence thesis;
        end;
       A28: for k holds P[k] from Ind(A17,A18);
       A29: 0< len v - m by A14,SQUARE_1:11;
       reconsider l = len v - m as Nat by A14,INT_1:18;
         m+l = len v by XCMPLX_1:27;
       hence contradiction by A3,A10,A11,A28,A29;
      case i<r & r=i+1;
       hence m+1 in dom v & v.(m+1) = i+1 by A13;
      end;
     hence thesis;
    case i=r; then m+1<=m by A9,A13; then 1<=m-m by REAL_1:84;
     then 1<=0 by XCMPLX_1:14;
     hence contradiction;
    end;
   hence thesis;
  end;

theorem
  v<>{} & rng v c= Seg n & v.1 = 1 & v.(len v) = n &
(for k st 1<=k & k<=len v - 1 holds
   for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s) implies
(for i st i in Seg n ex k st k in dom v & v.k = i) &
for m,k,i,r st m in dom v & v.m = i &
 (for j st j in dom v & v.j = i holds j<=m) &
             m<k & k in dom v & r = v.k holds i<r
 proof assume that
  A1: v<>{} and
  A2: rng v c= Seg n and
  A3: v.1 = 1 and
  A4: v.(len v) = n and
  A5: for k st 1<=k & k<=len v - 1 holds
        for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s;
    len v <> 0 by A1,FINSEQ_1:25;
  then 0 < len v by NAT_1:19;
then A6:  1<=1 & 0+1<=len v & len v<=len v by NAT_1:38;
  then A7: 1 in dom v & len v in dom v by FINSEQ_3:27;
  defpred P[Nat] means $1 in Seg n implies ex k st k in dom v & v.k = $1;
  A8: P[0] by FINSEQ_1:3;
  A9: for i st P[i] holds P[i+1]
   proof let i such that
    A10: i in Seg n implies ex k st k in dom v & v.k = i; assume
    A11: i+1 in Seg n;
       now per cases;
     suppose A12: i = 0;
      take k=1;
      thus k in dom v & v.k = i+1 by A3,A6,A12,FINSEQ_3:27;
     suppose i<>0; then 0<i by NAT_1:19;
      then 0+1<=i & i<=i+1 & i+1<=n by A11,FINSEQ_1:3,NAT_1:38;
then A13:      1<=i & i<=n by AXIOMS:22;
      then A14: i in Seg n by FINSEQ_1:3;
      defpred R[Nat] means $1 in dom v & v.$1 = i;
      A15: ex k st R[k] by A10,A13,FINSEQ_1:3;
      A16: for k holds R[k] implies k<=len v by FINSEQ_3:27;
      consider m such that
      A17: R[m] & for k st R[k] holds k<=m
         from Max(A16,A15);
      take k = m+1;
      thus k in dom v & v.k = i+1 by A1,A2,A4,A5,A11,A14,A17,Th14;
     end;
    hence thesis;
   end;
  thus for i holds P[i] from Ind(A8,A9);
  let m,k,i,r; assume
  A18: m in dom v & v.m = i & (for j st j in dom v & v.j = i holds j<=m) &
      m<k & k in dom v & r = v.k;
  then A19: 1<=m & m<=len v & 1<=k & k<=len v by FINSEQ_3:27;
A20: i in rng v by A18,FUNCT_1:def 5;
  then A21: 1<=i & i<=n & i<=i+1 by A2,FINSEQ_1:3,NAT_1:29;
     now per cases;
   suppose i=n;
    then len v<=m by A4,A7,A18;
    hence thesis by A18,A19,AXIOMS:21;
   suppose i<>n; then i<n by A21,REAL_1:def 5;
    then 1<=i+1 & i+1<=n by NAT_1:29,38;
    then i+1 in Seg n by FINSEQ_1:3;
    then A22: m+1 in dom v & v.(m+1) = i+1 by A1,A2,A4,A5,A18,A20,Th14;
    defpred P[set] means
    for j,s st j=$1 & j>0 & m+j in dom v & s=v.(m+j) holds i<s;
    A23: P[0];
    A24: for k st P[k] holds P[k+1]
     proof let k such that
      A25: P[k];
      let j,s such that
      A26: j=k+1 & j>0 & m+j in dom v & s=v.(m+j);
       per cases;
       suppose k=0;
        hence i<s by A22,A26,NAT_1:38;
       suppose k<>0;
        then A27: 0<k & m+(k+1)<=len v & m+k+1 = m+(k+1) & m+k<=m+k+1 & m<=m+k
           by A26,FINSEQ_3:27,NAT_1:19,29,XCMPLX_1:1;
        then A28: 1<=m+k & m+k<=len v & m+k<= len v - 1 by A19,AXIOMS:22,REAL_1
:84;
        then A29: m+k in dom v by FINSEQ_3:27;
        then v.(m+k) in rng v by FUNCT_1:def 5;
        then v.(m+k) in Seg n & Seg n c= NAT by A2;
        then reconsider r1=v.(m+k) as Nat;
          s in rng v by A26,FUNCT_1:def 5;
        then s in Seg n & Seg n c= NAT by A2;
        then reconsider s1=s as Nat;
        A30: i<r1 by A25,A27,A29;
           now per cases by A5,A26,A27,A28;
         suppose A31: abs(r1-s)=1;
             now per cases by A31,Th1;
           suppose r1>s & r1=s+1; then A32: i<=s1 by A30,NAT_1:38;
               now per cases by A32,REAL_1:def 5;
             case i<s; hence thesis;
             case s=i; then m+j<=m by A18,A26;
              then j<=m-m by REAL_1:84;
              hence contradiction by A26,XCMPLX_1:14;
             end;
            hence thesis;
           suppose r1<s & s=r1+1; hence i<s by A30,AXIOMS:22;
           end;
          hence thesis;
         suppose r1=s; hence thesis by A25,A27,A29;
         end;
        hence thesis;
     end;
    A33: for k holds P[k] from Ind(A23,A24);
    A34: 0< k - m & m<=k by A18,SQUARE_1:11;
    reconsider l = k - m as Nat by A18,INT_1:18;
      m+l = k by XCMPLX_1:27;
    hence i<r by A18,A33,A34;
   end;
  hence thesis;
 end;

theorem Th16:
i in dom f & 2<=len f implies f/.i in L~f
 proof assume
  A1: i in dom f & 2<=len f;
  then A2: 1<=i & i<=len f by FINSEQ_3:27;
  per cases by A2,REAL_1:def 5;
   suppose A3: i=len f;
    reconsider l=i-1 as Nat by A2,INT_1:18;
      1+1<=i & 0<=1 by A1,A3;
then A4:    1<=l & l<=i by PROB_1:2,REAL_1:84;
      l+1 = i by XCMPLX_1:27;
    then f/.(l+1) in LSeg(f,l) & LSeg(f,l) c=L~f
     by A2,A4,TOPREAL1:27,TOPREAL3:26;
    then f/.(l+1) in L~f;
    hence f/.i in L~f by XCMPLX_1:27;
   suppose i<len f;
    then 1<=i+1 & i+1<=len f by NAT_1:29,38;
    then f/.i in LSeg(f,i) & LSeg(f,i) c= L~f
     by A2,TOPREAL1:27,TOPREAL3:26;
    hence thesis;
 end;

begin
:::::::::::::::::::::::
:: Matrix preliminaries
:::::::::::::::::::::::

theorem Th17:
for D being non empty set,M being Matrix of D holds
for i,j st j in dom M & i in Seg width M holds Col(M,i).j = Line(M,j).i
 proof let D be non empty set,M be Matrix of D;
  let i,j; assume
  A1: j in dom M & i in Seg width M;
  hence Col(M,i).j = M*(j,i) by MATRIX_1:def 9
                  .= Line(M,j).i by A1,MATRIX_1:def 8;
 end;

definition let D be non empty set;
 let M be Matrix of D;
 redefine attr M is empty-yielding means
:Def5: 0 = len M or 0 = width M;
 compatibility
  proof
   consider n being Nat such that
A1:   for x being set st x in rng M
      ex s being FinSequence st s=x & len s = n by MATRIX_1:def 1;
   hereby assume
A2:  M is empty-yielding;
    consider s being Element of rng M;
    assume A3: 0 <> len M;
     then A4:   len M > 0 by NAT_1:19;
       M <> {} by A3,FINSEQ_1:25;
     then A5: rng M <> {} by FINSEQ_1:27;
     then ex p being FinSequence st p=s & len p = n by A1;
     then reconsider s as FinSequence;
       len s = 0 by A2,A5,MATRIX_1:def 2;
    hence 0 = width M by A4,A5,MATRIX_1:def 4;
   end;
   assume
A6: 0 = len M or 0 = width M;
   let s be set; assume
A7: s in rng M;
    then M <> {} by FINSEQ_1:27;
   then len M <> 0 by FINSEQ_1:25;
    then len M > 0 by NAT_1:19;
    then consider p being FinSequence such that
A8:   p in rng M and
A9:   len p = 0 by A6,MATRIX_1:def 4;
      ex q being FinSequence st q=p & len q = n by A1,A8;
    then ex q being FinSequence st q=s & len q = 0 by A1,A7,A9;
   hence Card s = 0;
  end;
end;

definition let M be Matrix of TOP-REAL 2;
attr M is X_equal-in-line means :Def6:
 for n st n in dom M holds X_axis(Line(M,n)) is constant;
attr M is Y_equal-in-column means :Def7:
 for n st n in Seg width M holds Y_axis(Col(M,n)) is constant;
attr M is Y_increasing-in-line means :Def8:
 for n st n in dom M holds Y_axis(Line(M,n)) is increasing;
attr M is X_increasing-in-column means :Def9:
 for n st n in Seg width M holds X_axis(Col(M,n)) is increasing;
end;

Lm1:
 for D being non empty set, M being Matrix of D
   holds M is non empty-yielding iff 0 < len M & 0 < width M
 proof let D be non empty set, M be Matrix of D;
  hereby assume M is non empty-yielding;
   then 0 <> len M & 0 <> width M by Def5;
   hence 0 < len M & 0 < width M by NAT_1:19;
  end;
  assume 0 < len M & 0 < width M;
  hence thesis by Def5;
 end;

definition
  cluster non empty-yielding X_equal-in-line Y_equal-in-column
    Y_increasing-in-line X_increasing-in-column Matrix of TOP-REAL 2;
 existence
  proof
   consider p;
   take M = <* <*p*> *>;
A1: len M=1 & width M=1 & Indices M=[:Seg 1,Seg 1 :] by MATRIX_1:25;
   hence M is non empty-yielding by Def5;
   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,m; assume k in dom L & m in dom L;
       then k in Seg len L & m in Seg len L & len L = len Line(M,n)
         by Def3,FINSEQ_1:def 3;
       then k in {1} & m in {1} by A1,FINSEQ_1:4,MATRIX_1:def 8;
       then k = 1 & m = 1 by TARSKI:def 1;
      hence L.k = L.m;
    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 k in dom L & m in dom L;
       then k in Seg len L & m in Seg len L & len L = len Col(M,n)
         by Def4,FINSEQ_1:def 3;
       then k in {1} & m in {1} by A1,FINSEQ_1:4,MATRIX_1:def 9;
       then k = 1 & m = 1 by TARSKI:def 1;
       hence L.k = L.m;
    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
       A2: k in dom L & m in dom L & k<m;
       then k in Seg len L & m in Seg len L & len L = len Line(M,n)
         by Def4,FINSEQ_1:def 3;
       then k in {1} & m in {1} by A1,FINSEQ_1:4,MATRIX_1:def 8;
       then k = 1 & m = 1 by TARSKI:def 1;
      hence L.k < L.m by A2;
    end;
   let n such that n in Seg width M;
     set L = X_axis(Col(M,n));
   let k,m; assume
       A3: k in dom L & m in dom L & k<m;
       then k in Seg len L & m in Seg len L & len L = len Col(M,n)
         by Def3,FINSEQ_1:def 3;
       then k in {1} & m in {1} by A1,FINSEQ_1:4,MATRIX_1:def 9;
       then k = 1 & m = 1 by TARSKI:def 1;
       hence L.k < L.m by A3;
  end;
end;

canceled;

theorem Th19:
for M being 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) & x in rng Line(M,m) &
       n in dom M & m in dom M & n<>m;
   A2: X_axis(Line(M,m)) is constant by A1,Def6;
   reconsider Ln = Line(M,n), Lm = Line(M,m) as FinSequence of TOP-REAL 2;
   consider i such that
   A3: i in dom Ln & Ln.i = x by A1,FINSEQ_2:11;
   reconsider Mi = Col(M,i) as FinSequence of TOP-REAL 2;
   consider j such that
   A4: j in dom Lm & Lm.j = x by A1,FINSEQ_2:11;
   A5: dom X_axis(Ln)=Seg len X_axis(Ln) & dom X_axis(Lm)=Seg len X_axis(Lm) &
       len Ln = width M & len Lm = width M by FINSEQ_1:def 3,MATRIX_1:def 8;
   set C = X_axis(Col(M,i));
   A6: len X_axis(Ln) = len Ln & len X_axis(Lm) = len Lm by Def3;
A7:  dom M = Seg len M by FINSEQ_1:def 3;
A8:  Seg len Ln = dom Ln & Seg len Lm = dom Lm by FINSEQ_1:def 3;
   then A9: C is increasing & len C = len Col(M,i) & len Col(M,i) = len M &
    dom C=Seg len C by A3,A5,Def3,Def9,FINSEQ_1:def 3,MATRIX_1:def 9;
   A10: Lm.i = M*(m,i) & Ln.i = M*(n,i) & Lm.j = M*(m,j) &
    Col(M,i).n = M*(n,i) & Col(M,i).m = M*(m,i)
     by A1,A3,A4,A5,A8,MATRIX_1:def 8,def 9;
   then reconsider p=x as Point of TOP-REAL 2 by A3;
   A11: i in dom X_axis(Lm) & j in dom X_axis(Lm) by A3,A4,A5,A8,Def3;
     i in dom Lm by A3,A5,FINSEQ_3:31;
then A12: Lm/.i = M*(m,i) by A10,FINSEQ_4:def 4;
A13: Lm/.j = p by A4,FINSEQ_4:def 4;
     i in dom(X_axis(Lm)) & j in dom(X_axis(Lm)) by A3,A4,A5,A6,FINSEQ_3:31;
   then (X_axis(Lm)).i = (X_axis(Lm)).j by A2,Def2;
then A14: (M*(m,i))`1 = (X_axis(Lm)).j by A3,A5,A6,A8,A12,Def3
               .= p`1 by A11,A13,Def3;
A15:  (M*(n,i))`1 = p`1 by A3,A5,A8,MATRIX_1:def 8;
     m in dom(Col(M,i)) by A1,A7,A9,FINSEQ_1:def 3;
then A16: M*(m,i) = Mi/.m by A10,FINSEQ_4:def 4;
     n in dom(Col(M,i)) by A1,A9,FINSEQ_3:31;
 then M*(n,i) = Mi/.n by A10,FINSEQ_4:def 4;
then A17: C.n = p`1 by A1,A7,A9,A15,Def3
       .= C.m by A1,A7,A9,A14,A16,Def3;
      n < m or m < n by A1,REAL_1:def 5;
   hence contradiction by A1,A7,A9,A17,Def1;
 end;

theorem Th20:
for M being 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) & x in rng Col(M,m) &
   n in Seg width M & m in Seg width M & n<>m;
   A2: Y_axis(Col(M,m)) is constant by A1,Def7;
   reconsider Ln = Col(M,n), Lm = Col(M,m) as FinSequence of TOP-REAL 2;
   consider i such that
   A3: i in dom Ln & Ln.i = x by A1,FINSEQ_2:11;
   reconsider Li = Line(M,i) as FinSequence of TOP-REAL 2;
   consider j such that
   A4: j in dom Lm & Lm.j = x by A1,FINSEQ_2:11;
   A5: dom Y_axis(Ln)=Seg len Y_axis(Ln) & dom Y_axis(Lm)=Seg len Y_axis(Lm) &
     len Ln=len M & len Lm=len M by FINSEQ_1:def 3,MATRIX_1:def 9;
   set C = Y_axis(Line(M,i));
   A6: len Y_axis(Ln) = len Ln & len Y_axis(Lm) = len Lm by Def4;
A7:  dom M = Seg len M by FINSEQ_1:def 3;
A8:  Seg len Ln = dom Ln & Seg len Lm = dom Lm by FINSEQ_1:def 3;
   then A9: C is increasing & len C = len Line(M,i) & len Line(M,i) = width M &
    dom C=Seg len C by A3,A5,A7,Def4,Def8,FINSEQ_1:def 3,MATRIX_1:def 8;
   A10: Lm.i=M*(i,m) & Ln.i=M*(i,n) & Lm.j=M*(j,m) & Line(M,i).n=M*(i,n) &
       Line(M,i).m=M*(i,m) by A1,A3,A4,A5,A7,A8,MATRIX_1:def 8,def 9
;
   then reconsider p=x as Point of TOP-REAL 2 by A3;
   A11: i in dom Y_axis(Lm) & j in dom Y_axis(Lm) by A3,A4,A5,A8,Def4;
     i in dom Lm by A3,A5,FINSEQ_3:31;
then A12: Lm/.i = M*(i,m) by A10,FINSEQ_4:def 4;
A13: Lm/.j = p by A4,FINSEQ_4:def 4;
     (Y_axis(Lm)).i = (Y_axis(Lm)).j by A2,A3,A4,A5,A6,A8,Def2;
then A14: (M*(i,m))`2 = (Y_axis(Lm)).j by A3,A5,A6,A8,A12,Def4
               .= p`2 by A11,A13,Def4;
A15:  (M*(i,n))`2 = p`2 by A3,A5,A7,A8,MATRIX_1:def 9;
     m in dom(Line(M,i)) by A1,A9,FINSEQ_1:def 3;
then A16: M*(i,m) = Li/.m by A10,FINSEQ_4:def 4;
     n in dom(Line(M,i)) by A1,A9,FINSEQ_1:def 3;
 then M*(i,n) = Li/.n by A10,FINSEQ_4:def 4;
then A17: C.n = p`2 by A1,A9,A15,Def4
       .= C.m by A1,A9,A14,A16,Def4;
      n < m or m < n by A1,REAL_1:def 5;
   hence contradiction by A1,A9,A17,Def1;
 end;

begin
:::::::::::::::::::::
:: Go board
:::::::::::::::::::::

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
  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
  A1: x=G*(m,k) & x=G*(i,j) & [m,k] in Indices G & [i,j] in Indices G;
    Indices G=[:dom G,Seg width G:] by MATRIX_1:def 5;
  then A2: m in dom G & i in dom G & k in Seg width G & j in Seg width G
     by A1,ZFMISC_1:106;
  then A3: x=Line(G,m).k & x=Col(G,k).m & x=Line(G,i).j & x=Col(G,j).i &
  len Line(G,m)=width G & len Line(G,i)=width G &
  len Col(G,k)=len G & len Col(G,j)=len G by A1,MATRIX_1:def 8,def 9;
    dom G = Seg len G &
  dom Line(G,m)=Seg len Line(G,m) & dom Line(G,i)=Seg len Line(G,i) &
  dom Col(G,k)=Seg len Col(G,k) & dom Col(G,j)=Seg len Col(G,j)
     by FINSEQ_1:def 3;
  then x in rng Line(G,m) & x in rng Line(G,i) &
  x in rng Col(G,k) & x in rng Col(G,j)
   by A2,A3,FUNCT_1:def 5;
  hence thesis by A2,Th19,Th20;
 end;

theorem
  m in dom f & f/.1 in rng Col(G,1) implies (f|m)/.1 in rng Col(G,1)
 proof assume
  A1: m in dom f & f/.1 in rng Col(G,1);
  then 1<=m by FINSEQ_3:27;
  then 1 in Seg m by FINSEQ_1:3;
  hence thesis by A1,Th10;
 end;

theorem
  m in dom f & f/.m in rng Col(G,width G) implies
 (f|m)/.len(f|m) in rng Col(G,width G)
 proof assume
  A1: m in dom f & f/.m in rng Col(G,width G);
  then 1<=m & m<=len f by FINSEQ_3:27;
  then len (f|m) = m & m in Seg m by FINSEQ_1:3,TOPREAL1:3;
  hence thesis by A1,Th10;
 end;

theorem Th24:
rng f misses rng Col(G,i) & f/.n = G*(m,k) & n in dom f & m in dom G
 implies i<>k
 proof assume that
A1: rng f /\ rng Col(G,i)={} and
A2: f/.n=G*(m,k) and
A3: n in dom f and
A4: m in dom G and
A5: i=k;
      f.n = G*(m,k) by A2,A3,FINSEQ_4:def 4;
then A6: G*(m,i) in rng f by A3,A5,FUNCT_1:def 5;
    dom G = Seg len G &
  dom Col(G,i)=Seg len Col(G,i) & len Col(G,i)=len G & Col(G,i).m=G*(m,i)
   by A4,FINSEQ_1:def 3,MATRIX_1:def 9;
  then G*(m,i) in rng Col(G,i) by A4,FUNCT_1:def 5;
  hence contradiction by A1,A6,XBOOLE_0:def 3;
 end;

definition let G,i;
assume A1: i in Seg width G & width G > 1;
func DelCol(G,i) -> Go-board means :Def10:
len it = len G & for k st k in dom G holds it.k = Del(Line(G,k),i);
 existence
  proof
   defpred P[Nat,Nat,Point of TOP-REAL 2] means $3 = Del(Line(G,$1),i).$2;
   A2: 0 < len G & 0 < width G by Lm1;
     0<>width G by Def5;
   then consider m such that
   A3: width G = m+1 by NAT_1:22;
A4:  Seg len G = dom G by FINSEQ_1:def 3;
   A5: for k st k in dom G holds len (Del(Line(G,k),i))=m
    proof let k such that k in dom G;
     A6: len (Line(G,k))= width G by MATRIX_1:def 8;
     then i in dom (Line(G,k)) by A1,FINSEQ_1:def 3;
     then ex j st len (Line(G,k))=j+1 & len Del(Line(G,k),i)=j by MATRIX_2:8;
     hence thesis by A3,A6,XCMPLX_1:2;
    end;
   A7: for k,j st [k,j] in [:Seg len G, Seg m:]
    for x1,x2 being Point of TOP-REAL 2 st P[k,j,x1] & P[k,j,x2] holds x1=x2;
   A8: for k,j st [k,j] in [:Seg len G, Seg m:]
      ex x being Point of TOP-REAL 2 st P[k,j,x]
    proof let k,j; assume [k,j] in [:Seg len G, Seg m:];
     then A9: k in dom G & j in Seg m by A4,ZFMISC_1:106;
     reconsider p=Del(Line(G,k),i) as FinSequence of TOP-REAL 2 by MATRIX_2:9;
        len p = m by A5,A9;
     then j in dom p by A9,FINSEQ_1:def 3;
     then reconsider x = p.j as Point of TOP-REAL 2 by FINSEQ_2:13;
     take x;
     thus thesis;
    end;
   consider N being Matrix of len G,m,the carrier of TOP-REAL 2 such that
   A10: for k,j st [k,j] in Indices N holds P[k,j,N*(k,j)]
    from MatrixEx(A7,A8);
A11:  Seg len N = dom N by FINSEQ_1:def 3;
   A12: len N = len G & width N = m & Indices N = [:dom G, Seg m:]
                                                         by A2,A4,MATRIX_1:24;
   A13: for k,j st k in dom G & j in Seg m holds N*(k,j)=Del(Line(G,k),i).j
    proof let k,j; assume k in dom G & j in Seg m;
     then [k,j] in Indices N by A12,ZFMISC_1:106;
     hence thesis by A10;
    end;
   A14: for k,j st k in dom G & j in Seg m holds
       N*(k,j)=Line(G,k).j or N*(k,j)=Line(G,k).(j+1)
    proof let k,j; assume
     A15: k in dom G & j in Seg m;
     then A16: N*(k,j)=Del(Line(G,k),i).j by A13;
     A17: len Line(G,k) = m+1 by A3,MATRIX_1:def 8;
       i in Seg len Line(G,k) by A1,MATRIX_1:def 8;
     then i in dom Line(G,k) by FINSEQ_1:def 3;
     hence thesis by A15,A16,A17,Th7;
    end;
   A18: 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
     A19: k in Seg m;
     then A20: 1<=k & k<=m by FINSEQ_1:3;
       m<=m+1 & k<=k+1 by NAT_1:29;
     then k<=m+1 & 1<=k+1 & k+1<=m+1 by A20,AXIOMS:22,24;
     then A21: k in Seg width G & k+1 in Seg width G by A3,A20,FINSEQ_1:3;
     A22: len Col(N,k) = len N & len Col(G,k)=len G &
         len Col(G,k+1) = len G by MATRIX_1:def 9;
        now per cases;
      suppose A23: k<i;
          now let j; assume 1<=j & j<=len Col(N,k);
         then A24: j in dom N by A22,FINSEQ_3:27;
         A25: len Line(G,j) = m+1 by A3,MATRIX_1:def 8;
         thus Col(N,k).j= N*(j,k) by A24,MATRIX_1:def 9
          .= Del(Line(G,j),i).k by A4,A11,A12,A13,A19,A24
          .= Line(G,j).k by A23,A25,Th8
          .= Col(G,k).j by A4,A11,A12,A21,A24,Th17;
        end;
       hence thesis by A12,A22,FINSEQ_1:18;
      suppose A26: k>=i;
          now let j; assume 1<=j & j<=len Col(N,k);
         then A27: j in dom N by A22,FINSEQ_3:27;
         A28: len Line(G,j) = m+1 by A3,MATRIX_1:def 8;
         A29: dom Line(G,j) = Seg len Line(G,j) by FINSEQ_1:def 3;
         thus Col(N,k).j= N*(j,k) by A27,MATRIX_1:def 9
          .= Del(Line(G,j),i).k by A4,A11,A12,A13,A19,A27
          .= Line(G,j).(k+1) by A1,A3,A20,A26,A28,A29,Th9
          .= Col(G,k+1).j by A4,A11,A12,A21,A27,Th17;
        end;
       hence thesis by A12,A22,FINSEQ_1:18;
      end;
     hence thesis;
    end;
   reconsider M=N as Matrix of TOP-REAL 2;
     1-1<m by A1,A3,REAL_1:84;
   then A30: 0<len M & 0<width M by A2,MATRIX_1:24;
   A31: now let k; assume A32: k in dom M;
     then A33: X_axis(Line(G,k)) is constant by A4,A11,A12,Def6;
       m<=m+1 by NAT_1:29;
     then A34: Seg m c= Seg width G by A3,FINSEQ_1:7;
     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 such that
       A35: n in dom X & j in dom X;
       A36: 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 Def3,FINSEQ_1:def 3,MATRIX_1:def 8;
       then A37: L.n = M*(k,n) & L.j=M*(k,j) & n in Seg m & j in Seg m
         by A2,A35,MATRIX_1:24,def 8;
       then A38: (L.n=lg.n or L.n=lg.(n+1)) & (L.j=lg.j or L.j=lg.(j+1))
        by A4,A11,A12,A14,A32;
         n in dom L & j in dom L by A35,A36,FINSEQ_1:def 3;
       then L.n = L/.n & L.j = L/.j by FINSEQ_4:def 4;
       then A39: X.n = M*(k,n)`1 & X.j=M*(k,j)`1 by A35,A37,Def3;
          1<=n & n<=m & 1<=j & j<=m by A12,A35,A36,FINSEQ_3:27;
       then A40: n<=n+1 & n+1<=m+1 & j<=j+1 & j+1<=m+1 by AXIOMS:24,NAT_1:29;
         1<=n+1 & 1<=j+1 by NAT_1:29;
       then A41: n+1 in Seg width G & j+1 in Seg width G &
        n in Seg width G & j in Seg width G
            by A3,A12,A34,A35,A36,A40,FINSEQ_3:27;
       then A42: 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_1:def 8;
         dom lg = Seg len xg by A36,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 A36,A41,FINSEQ_4:def 4;
       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 A36,A41,A42,Def3;
       hence X.n = X.j by A33,A36,A37,A38,A39,A41,A42,Def2;
      end;
     hence X_axis(Line(M,k)) is constant by Def2;
    end;
   A43: now let k; assume
     A44: k in Seg width M;
     then A45: Col(M,k)=Col(G,k) or Col(M,k)=Col(G,k+1) by A12,A18;
     A46: 1<=k & k<=m by A12,A44,FINSEQ_1:3;
       m<=m+1 & k<=k+1 by NAT_1:29;
     then k<=m+1 & 1<=k+1 & k+1<=m+1 by A46,AXIOMS:22,24;
     then k in Seg width G & k+1 in Seg width G by A3,A46,FINSEQ_1:3;
     hence Y_axis(Col(M,k)) is constant by A45,Def7;
    end;
   A47: now 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:29;
     then A48: Seg m c= Seg width G by A3,FINSEQ_1:7;
     assume
     A49: k in dom M;
     then A50: xg is increasing by A4,A11,A12,Def8;
        now let n,j such that
       A51: n in dom X & j in dom X & n<j;
       A52: 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 Def4,FINSEQ_1:def 3,MATRIX_1:def 8;
then A53:    L.n = M*(k,n) & L.j=M*(k,j) & n in Seg m & j in Seg m
         by A2,A51,MATRIX_1:24,def 8;
         dom L = Seg len X by A52,FINSEQ_1:def 3;
       then L.n = L/.n & L.j = L/.j by A51,A52,FINSEQ_4:def 4;
then A54:    X.n = M*(k,n)`2 & X.j=M*(k,j)`2 by A51,A53,Def4;
       A55: 1<=n & n<=m & 1<=j & j<=m by A12,A51,A52,FINSEQ_3:27;
       then A56: n<=n+1 & n+1<=m+1 & j<=j+1 & j+1<=m+1 by AXIOMS:24,NAT_1:29;
         1<=n+1 & 1<=j+1 by NAT_1:29;
       then A57: n+1 in Seg width G & j+1 in Seg width G &
         n in Seg width G & j in Seg width G
            by A3,A12,A48,A51,A52,A56,FINSEQ_3:27;
       then A58: 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_1:def 8;
         dom lg = Seg len xg by A52,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 A52,A57,FINSEQ_4:def 4;
then A59:    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 A52,A57,A58,Def4;
       set r = X.n, s = X.j;
       A60: dom lg = Seg len lg by FINSEQ_1:def 3;
        per cases;
        suppose A61: j<i;
         then A62: n<i by A51,AXIOMS:22;
         A63: M*(k,n) = (Del(lg,i)).n by A4,A11,A12,A13,A49,A51,A52
          .= G*(k,n) by A3,A52,A58,A62,Th8;
           M*(k,j) = (Del(lg,i)).j by A4,A11,A12,A13,A49,A51,A52
          .= G*(k,j) by A3,A52,A58,A61,Th8;
         hence r < s by A12,A48,A50,A51,A52,A54,A59,A63,Def1;
        suppose A64: j>=i;
         A65: M*(k,j) = (Del(lg,i)).j by A4,A11,A12,A13,A49,A51,A52
          .= G*(k,j+1) by A1,A3,A52,A55,A58,A60,A64,Th9;
            now per cases;
          suppose A66: n<i; j<=j+1 by NAT_1:29;
           then A67: n<j+1 by A51,AXIOMS:22;
             M*(k,n) = (Del(lg,i)).n by A4,A11,A12,A13,A49,A51,A52
            .= G*(k,n) by A3,A52,A58,A66,Th8;
           hence r < s by A50,A52,A54,A57,A59,A65,A67,Def1;
          suppose A68: n>=i;
           A69: n+1<j+1 by A51,REAL_1:53;
             M*(k,n) = (Del(lg,i)).n by A4,A11,A12,A13,A49,A51,A52
           .= G*(k,n+1) by A1,A3,A52,A55,A58,A60,A68,Th9;
           hence r < s by A50,A52,A54,A57,A59,A65,A69,Def1;
          end;
         hence r < s;
        end;
     hence Y_axis(Line(M,k)) is increasing by Def1;
    end;
      now let k; assume
     A70: k in Seg width M;
     then A71: Col(M,k)=Col(G,k) or Col(M,k)=Col(G,k+1) by A12,A18;
     A72: 1<=k & k<=m by A12,A70,FINSEQ_1:3;
       m<=m+1 & k<=k+1 by NAT_1:29;
     then k<=m+1 & 1<=k+1 & k+1<=m+1 by A72,AXIOMS:22,24;
     then k in Seg width G & k+1 in Seg width G by A3,A72,FINSEQ_1:3;
     hence X_axis(Col(M,k)) is increasing by A71,Def9;
    end;
   then reconsider M as non empty-yielding X_equal-in-line Y_equal-in-column
    Y_increasing-in-line X_increasing-in-column Matrix of TOP-REAL 2
        by A30,A31,A43,A47,Def5,Def6,Def7,Def8,Def9;
   take M;
   thus A73: len M = len G by A2,MATRIX_1:24;
   let k; assume
   A74: k in dom G;
   then A75: M.k = Line(M,k) by A4,A11,A73,MATRIX_2:18;
   then reconsider s = M.k as FinSequence;
   A76: len s= m by A12,A75,MATRIX_1:def 8;
   A77: len (Del(Line(G,k),i))=m by A5,A74;
      now let j; assume
     A78: j in Seg m;
     then Line(M,k).j=M*(k,j) by A12,MATRIX_1:def 8;
     hence s.j=Del(Line(G,k),i).j by A13,A74,A75,A78;
    end;
   hence thesis by A76,A77,FINSEQ_2:10;
  end;
 uniqueness
  proof let G1,G2 be Go-board; assume that
   A79: len G1=len G & for k st k in dom G holds G1.k=Del(Line(G,k),i) and
   A80: len G2=len G & for k st k in dom G holds G2.k=Del(Line(G,k),i);
      now let k; assume k in Seg len G;
     then A81: k in dom G by FINSEQ_1:def 3;
     hence G1.k = Del(Line(G,k),i) by A79
               .= G2.k by A80,A81;
    end;
   hence G1=G2 by A79,A80,FINSEQ_2:10;
  end;
end;

theorem Th25:
i in Seg width G & width G > 1 & k in dom G implies
Line(DelCol(G,i),k) = Del(Line(G,k),i)
 proof
  set D = DelCol(G,i); assume
  A1: i in Seg width G & width G >1 & k in dom G;
then A2:  len D = len G & D.k = Del(Line(G,k),i) by Def10;
  then dom D = dom G by FINSEQ_3:31;
  hence thesis by A1,A2,MATRIX_2:18;
 end;

theorem Th26:
i in Seg width G & width G = m+1 & m>0 implies width DelCol(G,i) = m
 proof
  set D = DelCol(G,i);
A1: dom Line(G,1) = Seg len Line(G,1) by FINSEQ_1:def 3;
  assume
  A2: i in Seg width G & width G = m+1 & m>0;
  then A3: 0+1<width G & 0<len G by Lm1,REAL_1:53;
  then 0+1<=len G by NAT_1:38;
  then 1 in dom G by FINSEQ_3:27;
  then Line(D,1) = Del(Line(G,1),i) & len Line(G,1) = m+1 & len Line(D,1) =
width D
       by A2,A3,Th25,MATRIX_1:def 8;
  hence thesis by A1,A2,Th6;
 end;

theorem
  i in Seg width G & width G > 1 implies width G = width DelCol(G,i) + 1
 proof assume
  A1: i in Seg width G & width G > 1;
  then ex m st width G = m+1 & m>0 by Th3;
  hence thesis by A1,Th26;
 end;

theorem Th28:
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
 proof assume
  A1: i in Seg width G & width G > 1 & n in dom G &
   m in Seg width (DelCol(G,i));
  hence DelCol(G,i)*(n,m) = Line(DelCol(G,i),n).m by MATRIX_1:def 8
   .= Del(Line(G,n),i).m by A1,Th25;
 end;

theorem Th29:
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
 proof
  set N = DelCol(G,i); assume
  A1: i in Seg width G & width G = m+1 & m>0 & 1<=k & k<i;
  then A2: 1<=i & i<=m+1 & width N = m by Th26,FINSEQ_1:3;
  then k<m+1 by A1,AXIOMS:22;
then A3:  k<=m+1 & k<=m by NAT_1:38;
  then A4: k in Seg width G & k in Seg width N by A1,A2,FINSEQ_1:3;
  A5: len Col(N,k) = len N & len Col(G,k)=len G by MATRIX_1:def 9;
  A6: 1<width G by A1,Th3;
  then A7: len N = len G by A1,Def10;
     now let j; assume 1<=j & j<=len Col(N,k);
    then A8: j in dom N by A5,FINSEQ_3:27;
A9: dom N = Seg len N & dom G = Seg len G by FINSEQ_1:def 3;
    A10: len Line(G,j) = m+1 by A1,MATRIX_1:def 8;
    thus Col(N,k).j= N*(j,k) by A8,MATRIX_1:def 9
     .= Del(Line(G,j),i).k by A1,A4,A6,A7,A8,A9,Th28
     .= Line(G,j).k by A1,A10,Th8
     .= Col(G,k).j by A4,A7,A8,A9,Th17;
   end;
  hence thesis by A1,A2,A3,A5,A7,FINSEQ_1:3,18;
 end;

theorem Th30:
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
 proof
  set N = DelCol(G,i); assume
  A1: i in Seg width G & width G = m+1 & m>0 & i<=k & k<=m;
  then A2: 1<=i & i<=m+1 & width N = m by Th26,FINSEQ_1:3;
then A3:  1<=k+1 & k+1<=m+1 & 1<=k by A1,AXIOMS:22,24,NAT_1:29;
  then A4: k+1 in Seg width G & k in Seg width N by A1,A2,FINSEQ_1:3;
  A5: len Col(N,k) = len N & len Col(G,k+1)=len G by MATRIX_1:def 9;
  A6: 1<width G by A1,Th3;
  then A7: len N = len G by A1,Def10;
     now let j; assume 1<=j & j<=len Col(N,k);
    then A8: j in dom N by A5,FINSEQ_3:27;
A9:  dom N = Seg len N & dom G = Seg len G by FINSEQ_1:def 3;
    A10: len Line(G,j) = m+1 by A1,MATRIX_1:def 8;
    A11: dom Line(G,j) = Seg len Line(G,j) by FINSEQ_1:def 3;
    thus Col(N,k).j= N*(j,k) by A8,MATRIX_1:def 9
     .= Del(Line(G,j),i).k by A1,A4,A6,A7,A8,A9,Th28
     .= Line(G,j).(k+1) by A1,A10,A11,Th9
     .= Col(G,k+1).j by A4,A7,A8,A9,Th17;
   end;
  hence thesis by A1,A2,A3,A5,A7,FINSEQ_1:3,18;
 end;

theorem Th31:
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
 proof assume
  A1: i in Seg width G & width G = m+1 & m>0 & n in dom G & 1<=k & k<i;
  then A2: Col(DelCol(G,i),k) = Col(G,k) &
    k in Seg width DelCol(G,i) & k in Seg width G
    by Th29;
A3: dom G = Seg len G & Seg len(DelCol(G,i)) = dom(DelCol(G,i))
   by FINSEQ_1:def 3;
    1<width G by A1,Th3;
  then len (DelCol(G,i)) = len G by A1,Def10;
  hence DelCol(G,i)*(n,k) = Col(G,k).n by A1,A2,A3,MATRIX_1:def 9
  .= G*(n,k) by A1,MATRIX_1:def 9;
  thus thesis by A1,Th29;
 end;

theorem Th32:
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
 proof assume
  A1: i in Seg width G & width G = m+1 & m>0 & n in dom G & i<=k & k<=m;
  then A2: Col(DelCol(G,i),k)=Col(G,k+1) &
   k in Seg width DelCol(G,i) & k+1 in Seg width G
    by Th30;
A3: dom G = Seg len G & Seg len(DelCol(G,i)) = dom(DelCol(G,i))
   by FINSEQ_1:def 3;
    1<width G by A1,Th3;
  then len (DelCol(G,i)) = len G by A1,Def10;
  hence DelCol(G,i)*(n,k) = Col(G,k+1).n by A1,A2,A3,MATRIX_1:def 9
  .= G*(n,k+1) by A1,MATRIX_1:def 9;
  thus thesis by A1,Th30;
 end;

theorem
  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
 proof assume
  A1: width G = m+1 & m>0 & k in Seg m;
  then 1<=width G by Th3;
  then 1 in Seg width G & 1<=k & k<=m by A1,FINSEQ_1:3;
  hence thesis by A1,Th30;
 end;

theorem
  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
 proof assume
  A1: width G = m+1 & m>0 & k in Seg m & n in dom G;
  then 1<=width G by Th3;
  then 1 in Seg width G & 1<=k & k<=m by A1,FINSEQ_1:3;
  hence thesis by A1,Th32;
 end;

theorem
  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)
 proof assume
  A1: width G = m+1 & m>0 & k in Seg m;
  then 1<=width G by Th3;
  then A2: width G in Seg width G &
   1<=k & k<=m & m<m+1 by A1,FINSEQ_1:3,NAT_1:38;
  then k<width G by A1,AXIOMS:22;
  hence thesis by A1,A2,Th29;
 end;

theorem Th36:
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
 proof assume
  A1: width G = m+1 & m>0 & k in Seg m & n in dom G;
  then 1<=width G by Th3;
  then A2: width G in Seg width G & 1<=k & k<=m & m<m+1
   by A1,FINSEQ_1:3,NAT_1:38;
  then k<width G by A1,AXIOMS:22;
  hence thesis by A1,A2,Th31;
 end;

theorem
  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)
 proof set D = DelCol(G,i); assume
  A1: 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;
  then consider j such that
  A2: j in dom Line(G,m) & f/.n=Line(G,m).j by FINSEQ_2:11;
A3: dom Line(G,m) = Seg len Line(G,m) by FINSEQ_1:def 3;
    len Line(G,m) = width G by MATRIX_1:def 8;
  then A4: f/.n=G*(m,j) & 1<=j & j<=width G & 1<=i & i<=width G &
      len Line(D,m)=width D & dom Line(D,m) = Seg len Line(D,m)
    by A1,A2,A3,FINSEQ_1:def 3,FINSEQ_3:27,MATRIX_1:def 8;
  then A5: j<>i by A1,Th24;
  consider M be Nat such that
  A6: width G = M+1 & M>0 by A1,Th3;
  A7: width D = M by A1,A6,Th26;
   per cases by A5,REAL_1:def 5;
   suppose A8: j<i;
    then A9: f/.n=D*(m,j) by A1,A4,A6,Th31;
      j<width G by A4,A8,AXIOMS:22;
    then j<=M by A6,NAT_1:38;
    then j in Seg width D by A4,A7,FINSEQ_1:3;
    then Line(D,m).j=f/.n & Line(D,m).j in rng Line(D,m)
     by A4,A9,FUNCT_1:def 5,MATRIX_1:def 8;
    hence thesis;
   suppose i<j;
    then A10: 1<j & i+1<=j by A4,AXIOMS:22,NAT_1:38;
    reconsider l=j-1 as Nat by A4,INT_1:18;
    A11: i<=l & l<=M & l+1=j by A4,A6,A10,REAL_1:84,86,XCMPLX_1:27;
    then A12: f/.n=D*(m,l) & 1<=l by A1,A4,A6,Th32,AXIOMS:22;
    then l in Seg width D by A7,A11,FINSEQ_1:3;
    then Line(D,m).l=f/.n & Line(D,m).l in rng Line(D,m)
       by A4,A12,FUNCT_1:def 5,MATRIX_1:def 8;
  hence thesis;
 end;

reserve D for set,
        f for FinSequence of D,
        M for Matrix of D;

definition let D,f,M;
pred f is_sequence_on M means :Def11:
 (for n st n in dom f 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
      abs(m-i)+abs(k-j) = 1);
end;

Lm2: <*>D is_sequence_on M
proof set f = <*>D;
 thus (for n st n in dom f 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 abs(m-i)+abs(k-j) = 1;
end;

theorem
   (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:27;
   hence thesis by TOPREAL1:3;
 end;
 assume
  A1: f is_sequence_on M;
 per cases;
  suppose m < 1;
   then m = 0 & f|0 = <*>D by RLVECT_1:98;
   hence thesis by Lm2;
  suppose m >= len f;
   hence thesis by A1,TOPREAL1:2;
  suppose A2: 1 <= m & m < len f;
   then A3: m in dom f by FINSEQ_3:27;
  A4: dom g = Seg len g & dom f = Seg len f by FINSEQ_1:def 3;
  A5: len g = m by A2,TOPREAL1:3;
  A6: now let n; assume A7: n in dom g;
     then n in dom f & g/.n=f/.n by A3,A4,A5,Th10;
    then consider i,j such that
    A8: [i,j] in Indices M & f/.n=M*(i,j) by A1,Def11;
    take i,j;
    thus [i,j] in Indices M & g/.n = M*(i,j) by A3,A4,A5,A7,A8,Th10;
   end;
     now let n; assume n in dom g & n+1 in dom g;
    then A9: g/.n=f/.n & g/.(n+1)=f/.(n+1) & n in dom f & n+1 in dom f
     by A3,A4,A5,Th10;
    let i1,i2,j1,j2 be Nat; assume
      [i1,i2] in Indices M & [j1,j2] in Indices M &
    g/.n=M*(i1,i2) & g/.(n+1)=M*(j1,j2);
    hence abs(i1-j1)+abs(i2-j2) = 1 by A1,A9,Def11;
   end;
  hence thesis by A6,Def11;
 end;

theorem
  (for n st n in dom f1 ex i,j st [i,j] in Indices M & f1/.n=M*(i,j)) &
(for n st n in dom f2 ex i,j st [i,j] in Indices M & f2/.n=M*(i,j)) implies
for n st n in dom(f1^f2) 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 ex i,j st [i,j] in Indices M & f1/.n=M*(i,j) and
  A2: for n st n in dom f2 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:38;
   suppose A4: n in dom f1;
    then consider i,j such that
    A5: [i,j] in Indices M & f1/.n=M*(i,j) by A1;
    take i,j;
    thus [i,j] in Indices M by A5;
    thus (f1^f2)/.n=M*(i,j) by A4,A5,GROUP_5:95;
   suppose ex m st m in dom f2 & n=len f1+m;
    then consider m such that
    A6: m in dom f2 & n=len f1+m;
    consider i,j such that
    A7: [i,j] in Indices M & f2/.m=M*(i,j) by A2,A6;
    take i,j;
    thus [i,j] in Indices M by A7;
    thus (f1^f2)/.n=M*(i,j) by A6,A7,GROUP_5:96;
 end;

theorem
  (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 abs(m-i)+abs(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 abs(m-i)+abs(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
   abs(m-i)+abs(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 abs(m-i)+abs(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 abs(m-i)+abs(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 abs(m-i)+abs(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
       abs(m-i)+abs(k-j)=1;
  let n such that
  A4: n in dom(f1^f2) & n+1 in dom(f1^f2);
  let m,k,i,j such that
  A5: [m,k] in Indices M & [i,j] in Indices M &
      (f1^f2)/.n=M*(m,k) & (f1^f2)/.(n+1)=M*(i,j);
  A6: dom(f1^f2)=Seg len(f1^f2) & dom f2=Seg len f2 & dom f1=Seg len f1
    by FINSEQ_1:def 3;
   per cases by A4,FINSEQ_1:38;
   suppose A7: n in dom f1;
    then A8: f1/.n=M*(m,k) & 1<=n & n<=len f1 by A5,A6,FINSEQ_1:3,GROUP_5:95;
       now per cases by A4,FINSEQ_1:38;
     suppose A9: n+1 in dom f1;
      then f1/.(n+1)=M*(i,j) by A5,GROUP_5:95;
      hence thesis by A1,A5,A7,A8,A9;
     suppose ex m st m in dom f2 & n+1=len f1+m;
      then consider mm be Nat such that
      A10: mm in dom f2 & n+1=len f1+mm;
        1<=mm by A10,FINSEQ_3:27;
      then A11: 0<=mm-1 by SQUARE_1:12;
        len f1+mm-1<=len f1 by A8,A10,XCMPLX_1:26;
      then len f1+(mm-1)<=len f1+0 by XCMPLX_1:29;
      then mm-1=0 by A11,REAL_1:53;
      then A12: mm=1 by XCMPLX_1:15;
      then A13: M*(i,j)=f2/.1 by A5,A10,GROUP_5:96;
      A14: n=len f1 by A10,A12,XCMPLX_1:2;
      then M*(m,k)=f1/.len f1 by A5,A7,GROUP_5:95;
      hence thesis by A3,A5,A7,A10,A12,A13,A14;
     end;
    hence thesis;
   suppose ex m st m in dom f2 & n=len f1+m;
    then consider mm be Nat such that
    A15: mm in dom f2 & n=len f1+mm;
       1<=mm & mm<=mm+1 & n+1<=len(f1^f2) by A4,A15,FINSEQ_3:27,NAT_1:29;
    then len f1+mm+1<=len f1+len f2 & len f1+mm+1=len f1+(mm+1)
      by A15,FINSEQ_1:35,XCMPLX_1:1;
    then 1<=mm+1 & mm+1<=len f2 by NAT_1:29,REAL_1:53;
    then A16: mm+1 in dom f2 by FINSEQ_3:27;
    A17: M*(i,j)=(f1^f2)/.(len f1+(mm+1)) by A5,A15,XCMPLX_1:1
    .=f2/.(mm+1) by A16,GROUP_5:96;
      M*(m,k)=f2/.mm by A5,A15,GROUP_5:96;
    hence thesis by A2,A5,A15,A16,A17;
 end;

reserve f for FinSequence of TOP-REAL 2;

theorem
  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
  A1: f is_sequence_on G & i in Seg width G & rng f misses rng Col(G,i) &
      width G > 1;
  then A2: len G = len D by Def10;
  consider M be Nat such that
  A3: width G = M+1 & M>0 by A1,Th3;
  A4: 1<=i & i<=width G by A1,FINSEQ_1:3;
  A5: width D = M by A1,A3,Th26;
A6: dom G = Seg len G & dom D = Seg len D by FINSEQ_1:def 3;
  A7: Indices G = [:dom G,Seg width G:] &
     Indices D = [:dom D,Seg width D:] by MATRIX_1:def 5;
  A8: now let n; assume A9: n in dom f; then consider m,k such that
    A10: [m,k] in Indices G & f/.n=G*(m,k) by A1,Def11;
    A11: m in dom G & k in Seg width G by A7,A10,ZFMISC_1:106;
    then A12: 1<=k & k<=M+1 by A3,FINSEQ_1:3;
    take m;
       now per cases;
      suppose A13: k<i;
      take k;
        k<width G by A4,A13,AXIOMS:22;
      then k<=M by A3,NAT_1:38;
      then k in Seg M by A12,FINSEQ_1:3;
      hence [m,k] in Indices D & f/.n=D*(m,k)
       by A1,A2,A3,A5,A6,A7,A10,A11,A12,A13,Th31,ZFMISC_1:106;
      suppose A14: i<=k;
        i<>k by A1,A9,A10,A11,Th24;
      then i<k by A14,REAL_1:def 5;
then A15:   i+1<=k & 1<k by A4,AXIOMS:22,NAT_1:38;
      then A16: i<=k-1 & 1<=k by REAL_1:84;
      reconsider l = k-1 as Nat by A15,INT_1:18;
      take l;
        1<=l & l<=M by A4,A12,A16,AXIOMS:22,REAL_1:86;
      then l in Seg M & D*(m,l)=G*(m,l+1) by A1,A3,A11,A16,Th32,FINSEQ_1:3;
      hence [m,l] in Indices D & f/.n=D*(m,l)
        by A2,A5,A6,A7,A10,A11,XCMPLX_1:27,ZFMISC_1:106;
     end;
    hence ex k st [m,k] in Indices D & f/.n=D*(m,k);
   end;
     now let n such that
    A17: n in dom f & n+1 in dom f;
    let i1,i2,j1,j2 be Nat; assume
    A18: [i1,i2] in Indices D & [j1,j2] in Indices D & f/.n = D*(i1,i2) &
        f/.(n+1) = D*(j1,j2);
    then A19: i1 in dom D & i2 in Seg width D & j1 in dom D & j2 in Seg width D
       by A7,ZFMISC_1:106;
    then A20: 1<=i2 & i2<=M & 1<=j2 & j2<=M & i2<=i2+1 & j2<=j2+1 & M<=M+1
     by A5,FINSEQ_1:3,NAT_1:29;
    then 1<=i2+1 & i2+1<=M+1 & 1<=j2+1 & j2+1<=M+1 by AXIOMS:22,24;
    then A21: i2+1 in Seg(M+1) & j2+1 in Seg(M+1) by FINSEQ_1:3;
      Seg width D c= Seg width G by A3,A5,A20,FINSEQ_1:7;
    then A22: [i1,i2] in Indices G & [j1,j2] in Indices G &
     [i1,i2+1] in Indices G & [j1,j2+1] in Indices G
      by A2,A3,A6,A7,A19,A21,ZFMISC_1:106;
       now per cases;
     case i2<i & j2<i;
      then f/.n=G*(i1,i2) & f/.(n+1)=G*
(j1,j2) by A1,A2,A3,A6,A18,A19,A20,Th31;
      hence abs(i1-j1)+abs(i2-j2) = 1 by A1,A17,A22,Def11;
     case A23: i<=i2 & j2<i;
      then f/.n=G*(i1,i2+1) & f/.(n+1)=G*(j1,j2)
       by A1,A2,A3,A6,A18,A19,A20,Th31,Th32;
      then A24: 1=abs(i1-j1)+abs(i2+1-j2) by A1,A17,A22,Def11;
        i2<=i2+1 by NAT_1:29; then i<=i2+1 by A23,AXIOMS:22;
      then j2<i2+1 by A23,AXIOMS:22;
      then j2+1<=i2+1 & 0<i2+1-j2 by NAT_1:38,SQUARE_1:11;
      then A25: 1<=i2+1-j2 & abs(i2+1-j2) = i2+1-j2 & 0<=abs(i1-j1)
         by ABSVALUE:5,def 1,REAL_1:84;
      then 0+(i2+1-j2)<=1 by A24,REAL_1:55;
      then i2+1-j2 = 1 by A25,AXIOMS:21;
      then i2+1=j2+1 by XCMPLX_1:27;
      hence contradiction by A23,XCMPLX_1:2;
     case A26: i2<i & i<=j2;
      then f/.n=G*(i1,i2) & f/.(n+1)=G*(j1,j2+1)
       by A1,A2,A3,A6,A18,A19,A20,Th31,Th32;
      then A27: 1=abs(i1-j1)+abs(i2-(j2+1)) by A1,A17,A22,Def11
          .=abs(i1-j1)+abs(-(j2+1 -i2)) by XCMPLX_1:143
          .=abs(i1-j1)+abs(j2+1 -i2) by ABSVALUE:17;
        j2<=j2+1 by NAT_1:29; then i<=j2+1 by A26,AXIOMS:22;
      then i2<j2+1 by A26,AXIOMS:22;
      then i2+1<=j2+1 & 0<j2+1-i2 by NAT_1:38,SQUARE_1:11;
      then A28: 1<=j2+1-i2 & abs(j2+1-i2) = j2+1-i2 & 0<=abs(i1-j1)
         by ABSVALUE:5,def 1,REAL_1:84;
      then 0+(j2+1-i2)<=1 by A27,REAL_1:55;
      then j2+1-i2 = 1 by A28,AXIOMS:21;
      then j2+1=i2+1 by XCMPLX_1:27;
      hence contradiction by A26,XCMPLX_1:2;
     case i<=i2 & i<=j2;
      then f/.n=G*(i1,i2+1) &
      f/.(n+1)=G*(j1,j2+1) by A1,A2,A3,A6,A18,A19,A20,Th32;
      hence 1 = abs(i1-j1)+abs((i2+1)-(j2+1)) by A1,A17,A22,Def11
      .= abs(i1-j1)+abs(i2-j2) by XCMPLX_1:32;
     end;
    hence abs(i1-j1)+abs(i2-j2) = 1;
   end;
  hence thesis by A8,Def11;
 end;

theorem Th42:
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 & f/.i=G*(n,m) by Def11;
  take n;
  set L = Line(G,n);
  A2: Indices G=[:dom G,Seg width G:] by MATRIX_1:def 5;
  hence n in dom G by A1,ZFMISC_1:106;
  A3: m in Seg width G by A1,A2,ZFMISC_1:106;
  then A4: L.m = f/.i & len L = width G by A1,MATRIX_1:def 8;
  then m in dom L by A3,FINSEQ_1:def 3;
  hence f/.i in rng L by A4,FUNCT_1:def 5;
 end;

theorem Th43:
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 abs(n-k) = 1
 proof assume
  A1: 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);
  then consider i1,i2 be Nat such that
  A2: [i1,i2] in Indices G & f/.i=G*(i1,i2) by Def11;
  consider j1,j2 be Nat such that
  A3: [j1,j2] in Indices G & f/.(i+1)=G*(j1,j2) by A1,Def11;
    Indices G=[:dom G,Seg width G:] by MATRIX_1:def 5;
  then A4: i1 in dom G & i2 in Seg width G &
      j1 in dom G & j2 in Seg width G by A2,A3,ZFMISC_1:106;
  then A5: Line(G,i1).i2 = f/.i & len Line(G,i1) = width G &
      Line(G,j1).j2=f/.(i+1) &
      len Line(G,j1) = width G by A2,A3,MATRIX_1:def 8;
then A6:  i2 in dom Line(G,i1) & j2 in dom Line(G,j1) by A4,FINSEQ_1:def 3;
  then A7: f/.i in rng Line(G,i1) & f/.(i+1) in rng Line(G,j1)
   by A5,FUNCT_1:def 5;
  then i1=n by A1,A4,Th19;
then A8:  abs(n-j1)+abs(i2-j2) = 1 by A1,A2,A3,Def11;
     now per cases by A8,Th2;
   suppose abs(n-j1)=1 & i2=j2;
    hence thesis by A4,A7,Th19;
   suppose abs(i2-j2)=1 & n=j1;
    hence thesis by A5,A6,FUNCT_1:def 5;
   end;
  hence thesis;
 end;

theorem Th44:
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 & f/.len f in rng Line(G,len G) and
  A2: f is_sequence_on G and
  A3: i in dom G and
  A4: i+1 in dom G and
  A5: m in dom f and
  A6: f/.m in rng Line(G,i) and
  A7: for k st k in dom f & f/.k in rng Line(G,i) holds k<=m;
A8: dom G = Seg len G by FINSEQ_1:def 3;
  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 & f/.n = G*(i,j) by A2,A10,Def11;
       [i,j] in [:dom G, Seg width G:] by A12,MATRIX_1:def 5;
     then i in dom G & j in Seg width G by ZFMISC_1:106;
     then A13: not f/.n in rng Line(G,i) & (Line(G,i)).j = G*(i,j) &
         j in Seg len Line(G,i) by A11,MATRIX_1:def 8;
     then j in dom Line(G,i) by FINSEQ_1:def 3;
     hence contradiction by A12,A13,FUNCT_1:def 5;
    end;
  defpred P[Nat,set] means
  $2 in dom G & for k st k=$2 holds f/.$1 in rng Line(G,k);
  A14: for n st n in Seg len f ex r st P[n,r]
    proof let n; assume n in Seg len f;
     then n in dom f by FINSEQ_1:def 3;
     then consider k such that
     A15: k in dom G & f/.n in rng Line(G,k) by A9;
     take r=k;
     thus r in dom G by A15;
     let m; assume m=r;
     hence f/.n in rng Line(G,m) by A15;
    end;
  consider v such that
  A16: dom v = Seg len f and
  A17: for n st n in Seg len f holds P[n,v.n]
   from SeqDEx(A14);
A18: len v = len f by A16,FINSEQ_1:def 3;
  A19: dom v = Seg len v & dom f = Seg len f & dom f c= NAT &
      dom G c= NAT by FINSEQ_1:def 3;
    1<=m & m<=len f by A5,FINSEQ_3:27;
  then 1<=1 & 1<=len f & len f<=len f by AXIOMS:22;
  then A20: 1 in dom f & len f in dom f by FINSEQ_3:27;
  reconsider p=f/.len f, q=f/.m as Point of TOP-REAL 2;
  A21: v<>{}
    proof assume v = {};
     then len v = 0 & 1<=len f by A1,FINSEQ_1:25;
     hence contradiction by A18;
    end;
  A22: rng v c= dom G
    proof let x; assume x in rng v;
     then ex y be Nat st y in dom v & v.y=x by FINSEQ_2:11;
     hence x in dom G by A16,A17;
    end;
  A23: v.(len v) = len G
    proof assume
     A24: v.(len v) <> len G;
     A25: v.(len v) in dom G &
       for k st k=v.(len v) holds f/.len v in rng Line(G,k)
        by A17,A18,A19,A20;
     then reconsider k=v.(len v) as Nat;
     A26: p in rng Line(G,k) by A17,A18,A19,A20; 0<len G by Lm1;
     then 0+1<=len G & len G<=len G by NAT_1:38;
     then len G in dom G by FINSEQ_3:27;
     hence contradiction by A1,A24,A25,A26,Th19;
    end;
  A27: for k st 1<=k & k<=len v - 1 holds
   for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s
    proof let k; assume
     A28: 1<=k & k<=len v - 1;
     then k<=k+1 & k+1<=len v by NAT_1:29,REAL_1:84;
     then 1<=k+1 & k+1<=len f & 1<=k & k<=len f by A18,A28,AXIOMS:22;
     then A29: k in dom f & k+1 in dom f by FINSEQ_3:27;
     let r,s; assume
     A30: r = v.k & s = v.(k+1);
then A31: r in rng v & s in rng v by A16,A19,A29,FUNCT_1:def 5;
      then r in dom G & s in dom G by A22;
     then reconsider n1=r, n2=s as Nat;
     set L1 = Line(G,n1),
         L2 = Line(G,n2);
A32:   dom L1 = Seg len L1 & Seg len L2 = dom L2 by FINSEQ_1:def 3;
     A33: f/.k in rng L1 & f/.(k+1) in rng L2 by A17,A19,A29,A30;
     then consider x be Nat such that
     A34: x in dom L1 & L1.x = f/.k by FINSEQ_2:11;
     A35: len L1 = width G & len L2 = width G by MATRIX_1:def 8;
     then A36: f/.k = G*(n1,x) by A32,A34,MATRIX_1:def 8;
     consider y be Nat such that
     A37: y in dom L2 & L2.y = f/.(k+1) by A33,FINSEQ_2:11;
     A38: f/.(k+1) = G*(n2,y) by A32,A35,A37,MATRIX_1:def 8;
       [n1,x] in [:dom G,Seg width G:] &
     [n2,y] in [:dom G,Seg width G:]
     by A22,A31,A32,A34,A35,A37,ZFMISC_1:106;
     then [n1,x] in Indices G & [n2,y] in Indices G by MATRIX_1:def 5;
     then abs(n1-n2)+abs(x-y)= 1 by A2,A29,A36,A38,Def11;
     hence thesis by Th2;
    end;
  A39: v.m = i
    proof assume
     A40: v.m <> i;
     A41: v.m in dom G &
       for k st k=v.m holds f/.m in rng Line(G,k) by A5,A17,A19;
     then reconsider k=v.m as Nat;
        q in rng Line(G,k) by A5,A17,A19;
     hence contradiction by A3,A6,A40,A41,Th19;
    end;
A42:   for k st k in dom v & v.k = i holds k<=m
    proof let k; assume
     A43: k in dom v & v.k=i;
     then f/.k in rng Line(G,i) by A16,A17;
     hence thesis by A7,A16,A19,A43;
    end;
  then A44: m+1 in dom v & v.(m+1)=i+1
  by A3,A4,A5,A8,A16,A19,A21,A22,A23,A27,A39,Th14;
  thus m+1 in dom f by A3,A4,A5,A8,A16,A19,A21,A22,A23,A27,A39,A42,Th14;
  thus thesis by A16,A17,A44;
 end;

theorem
  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 & f/.1 in rng Line(G,1) and
  A2: f/.len f in rng Line(G,len G) and
  A3: f is_sequence_on G;
  A4: 1 in dom f & len f in dom f by A1,FINSEQ_3:27;
   defpred P[Nat] means 1<=$1 & $1<= len G implies
     ex k st k in dom f & f/.k in rng Line(G,$1);
  A5: P[0];
  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
     A8: 1<=k+1 & k+1<=len G;
     then A9: k+1 in dom G by FINSEQ_3:27;
      per cases;
      suppose A10: k=0;
       take i=1;
       thus i in dom f & f/.i in rng Line(G,k+1) by A1,A10,FINSEQ_3:27;
      suppose k<>0; then 0<k & k<=k+1 by NAT_1:19,29;
       then A11: 0+1<=k & k<=len G by A8,NAT_1:38;
       defpred R[Nat] means $1 in dom f & f/.$1 in rng Line(G,k);
       A12: ex i st R[i] by A7,A11;
       A13: for i holds R[i] implies i<=len f by FINSEQ_3:27;
       A14: k in dom G by A11,FINSEQ_3:27;
       consider m such that
       A15: R[m] & for i st R[i] holds i<= m from Max(A13,A12);
       take n = m+1;
       thus n in dom f &
f/.n in rng Line(G,k+1) by A1,A2,A3,A9,A14,A15,Th44;
    end;
  thus A16: for i holds P[i] from Ind(A5,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 A17: 1<=i & i<=len G & 2<=len f;
   then consider k such that
    A18: k in dom f & f/.k in rng Line(G,i) by A16;
      f/.k in L~f by A17,A18,Th16;
    then L~f /\ rng Line(G,i) <> {} by A18,XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:def 7;
   end;
  let m,k,i,j; assume
  A19: 1<=m & m<=len G & 1<=k & k<=len G & i in dom f & j in dom f &
      f/.i in rng Line(G,m) &
      (for n st n in dom f & f/.n in rng Line(G,m) holds n<=i) & i<j &
      f/.j in rng Line(G,k);
  then A20: 1<=i & i<=len f & 1<=j & j<=len f by FINSEQ_3:27;
     now per cases;
   case m = len G; then len f<=i by A2,A4,A19;
    hence contradiction by A19,A20,AXIOMS:21;
   case m <> len G; then m<len G by A19,REAL_1:def 5;
    then 1<=m+1 & m+1<=len G by NAT_1:29,38;
    then m+1 in dom G & m in dom G by A19,FINSEQ_3:27;
    then A21: i+1 in dom f & f/.(i+1) in rng Line(G,m+1) & m+1 in dom G
      by A1,A2,A3,A19,Th44;
    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;
    A22: P[0];
    A23: for o be Nat st P[o] holds P[o+1]
     proof let o be Nat such that
      A24: P[o]; let n,l be Nat such that
      A25: n=o+1 & n>0 & i+n in dom f &
f/.(i+n) in rng Line(G,l) & l in dom G;
         now per cases;
       suppose o=0;
        then l=m+1 & m<m+1 by A21,A25,Th19,NAT_1:38;
        hence m<l;
       suppose o<>0;
        then A26: 0<o by NAT_1:19;
        A27: 1<=i & i+n<=len f & i+n = i+o+1 & i+o<=i+o+1 & i<=i+o
          by A19,A25,FINSEQ_3:27,NAT_1:37,XCMPLX_1:1;
        then 1<=i+o & i+o<=len f by AXIOMS:22;
        then A28: i+o in dom f by FINSEQ_3:27;
        then consider l1 be Nat such that
        A29: l1 in dom G & f/.(i+o) in rng Line(G,l1) by A3,Th42;
        A30: m<l1 by A24,A26,A28,A29;
           now per cases by A3,A25,A27,A28,A29,Th43;
         suppose f/.(i+n) in rng Line(G,l1);
          hence m<l by A25,A29,A30,Th19;
         suppose for k st f/.(i+n) in rng Line(G,k) & k in dom G
              holds abs(l1-k) = 1;
then A31:          abs(l1-l) = 1 by A25;
             now per cases by A31,Th1;
           suppose l1>l & l1=l+1;
then A32:            m<=l by A30,NAT_1:38;
               now per cases by A32,REAL_1:def 5;
             case m=l;
              then i+n<=i by A19,A25;
              then n<=i-i by REAL_1:84;
              hence contradiction by A25,XCMPLX_1:14;
             case m<l;
              hence thesis;
             end;
            hence thesis;
           suppose l1<l & l=l1+1;
            hence thesis by A30,AXIOMS:22;
           end;
          hence thesis;
         end;
        hence thesis;
       end;
      hence thesis;
     end;
    A33: for o be Nat holds P[o] from Ind(A22,A23);
    A34: 0< j - i & i<=j by A19,SQUARE_1:11;
    reconsider l = j - i as Nat by A19,INT_1:18;
      i+l = j & k in dom G by A19,FINSEQ_3:27,XCMPLX_1:27;
    hence m<k by A19,A33,A34;
   end;
  hence thesis;
 end;

theorem Th46:
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 & f/.i=G*(n,m) by Def11;
  take m;
  set L = Col(G,m);
  A2: Indices G=[:dom G,Seg width G:] by MATRIX_1:def 5;
  hence m in Seg width G by A1,ZFMISC_1:106;
  A3: n in dom G by A1,A2,ZFMISC_1:106;
  then A4: L.n = f/.i & len L = len G by A1,MATRIX_1:def 9;
  then n in dom L by A3,FINSEQ_3:31;
  hence f/.i in rng L by A4,FUNCT_1:def 5;
 end;

theorem Th47:
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 abs(n-k) = 1
 proof assume
  A1: 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); then consider i1,i2 be Nat such that
  A2: [i1,i2] in Indices G & f/.i=G*(i1,i2) by Def11;
  consider j1,j2 be Nat such that
  A3: [j1,j2] in Indices G & f/.(i+1)=G*(j1,j2) by A1,Def11;
    Indices G=[:dom G,Seg width G:] by MATRIX_1:def 5;
  then A4: i1 in dom G & i2 in Seg width G &
      j1 in dom G & j2 in Seg width G by A2,A3,ZFMISC_1:106;
  then A5: Col(G,i2).i1 = f/.i & len Col(G,i2) = len G & Col(G,j2).j1=f/.(i+1)
&
      len Col(G,j2) = len G by A2,A3,MATRIX_1:def 9;
then A6:  i1 in dom Col(G,i2) & j1 in dom Col(G,j2) by A4,FINSEQ_3:31;
then A7: f/.i in rng Col(G,i2) & f/.(i+1) in rng Col(G,j2) by A5,FUNCT_1:def 5
;
  then i2=n by A1,A4,Th20;
then A8:  abs(i1-j1)+abs(n-j2) = 1 by A1,A2,A3,Def11;
     now per cases by A8,Th2;
   suppose abs(i1-j1)=1 & n=j2;
    hence thesis by A5,A6,FUNCT_1:def 5;
   suppose abs(n-j2)=1 & i1=j1;
    hence thesis by A4,A7,Th20;
   end;
  hence thesis;
 end;

theorem Th48:
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 & f/.len f in rng Col(G,width G) and
  A2: f is_sequence_on G and
  A3: i in Seg width G and
  A4: i+1 in Seg width G and
  A5: m in dom f and
  A6: f/.m in rng Col(G,i) and
  A7: for k st k in dom f & f/.k in rng Col(G,i) holds k<=m;
A8: dom G = Seg len G by FINSEQ_1:def 3;
  A9: for n st n in dom f ex k st k in Seg width G & f/.n in rng Col(G,k)
    proof assume not thesis; then consider n such that
     A10: n in dom f and
     A11: for k st k in Seg width G holds not f/.n in rng Col(G,k);
     consider i,j such that
     A12: [i,j] in Indices G & f/.n = G*(i,j) by A2,A10,Def11;
       [i,j] in [:dom G, Seg width G:] by A12,MATRIX_1:def 5;
     then i in dom G & j in Seg width G by ZFMISC_1:106;
     then A13: not f/.n in rng Col(G,j) & (Col(G,j)).i = G*(i,j) &
         i in Seg len Col(G,j) by A8,A11,MATRIX_1:def 9;
     then i in dom Col(G,j) by FINSEQ_1:def 3;
     hence contradiction by A12,A13,FUNCT_1:def 5;
    end;
  defpred P[Nat,set] means
  $2 in Seg width G & for k st k=$2 holds f/.$1 in rng Col(G,k);
  A14: for n st n in Seg len f ex r st P[n,r]
    proof let n; assume n in Seg len f;
     then n in dom f by FINSEQ_1:def 3;
     then consider k such that
     A15: k in Seg width G & f/.n in rng Col(G,k) by A9;
     take r=k;
     thus r in Seg width G by A15;
     let m; assume m=r;
     hence f/.n in rng Col(G,m) by A15;
    end;
  consider v such that
  A16: dom v = Seg len f and
  A17: for n st n in Seg len f holds P[n,v.n] from SeqDEx(A14);
A18: len v = len f by A16,FINSEQ_1:def 3;
  A19: dom v = Seg len v & dom f = Seg len f & dom f c= NAT &
      Seg width G c= NAT by FINSEQ_1:def 3;
    1<=m & m<=len f by A5,FINSEQ_3:27;
  then 1<=1 & 1<=len f & len f<=len f by AXIOMS:22;
  then A20: 1 in dom f & len f in dom f by FINSEQ_3:27;
  A21: v<>{}
    proof assume v = {};
     then len v = 0 & 1<=len f by A1,FINSEQ_1:25;
     hence contradiction by A18;
    end;
  A22: rng v c= Seg width G
    proof let x; assume x in rng v;
      then ex y be Nat st y in dom v & v.y=x by FINSEQ_2:11;
     hence x in Seg width G by A16,A17;
    end;
  A23: v.(len v) = width G
    proof assume
     A24: v.(len v) <> width G;
     A25: v.(len v) in Seg width G &
       for k st k=v.(len v) holds f/.len v in rng Col(G,k)
        by A17,A18,A19,A20;
     then reconsider k=v.(len v) as Nat;
     A26: f/.len f in rng Col(G,k) by A17,A18,A19,A20; 0<width G by Lm1;
     then 0+1<=width G by NAT_1:38;
     then width G in Seg width G by FINSEQ_1:3;
     hence contradiction by A1,A24,A25,A26,Th20;
    end;
  A27: for k st 1<=k & k<=len v - 1 holds
   for r,s st r = v.k & s = v.(k+1) holds abs(r-s) = 1 or r=s
    proof let k; assume
     A28: 1<=k & k<=len v - 1;
     then k<=k+1 & k+1<=len v by NAT_1:29,REAL_1:84;
     then 1<=k+1 & k+1<=len f & 1<=k & k<=len f by A18,A28,AXIOMS:22;
     then A29: k in dom f & k+1 in dom f by FINSEQ_3:27;
     let r,s; assume
     A30: r = v.k & s = v.(k+1);
then A31: r in rng v & s in rng v by A16,A19,A29,FUNCT_1:def 5;
      then r in Seg width G & s in Seg width G by A22;
     then reconsider n1=r, n2=s as Nat;
     set L1 = Col(G,n1),
         L2 = Col(G,n2);
A32:   dom L1 = Seg len L1 & dom L2 = Seg len L2 by FINSEQ_1:def 3;
     A33: f/.k in rng L1 & f/.(k+1) in rng L2 by A17,A19,A29,A30;
     then consider x be Nat such that
     A34: x in dom L1 & L1.x = f/.k by FINSEQ_2:11;
     A35: len L1 = len G & len L2 = len G by MATRIX_1:def 9;
     then A36: f/.k = G*(x,n1) by A8,A32,A34,MATRIX_1:def 9;
     consider y be Nat such that
     A37: y in dom L2 & L2.y = f/.(k+1) by A33,FINSEQ_2:11;
     A38: f/.(k+1) = G*(y,n2) by A8,A32,A35,A37,MATRIX_1:def 9;
       [x,n1] in [:dom G,Seg width G:] &
     [y,n2] in [:dom G,Seg width G:]
     by A8,A22,A31,A32,A34,A35,A37,ZFMISC_1:106;
     then [x,n1] in Indices G & [y,n2] in Indices G by MATRIX_1:def 5;
     then abs(x-y)+abs(n1-n2)= 1 by A2,A29,A36,A38,Def11;
     hence thesis by Th2;
    end;
  A39: v.m = i
    proof assume
     A40: v.m <> i;
     A41: v.m in Seg width G &
       for k st k=v.m holds f/.m in rng Col(G,k) by A5,A17,A19;
     then reconsider k=v.m as Nat;
       f/.m in rng Col(G,k) by A5,A17,A19;
     hence contradiction by A3,A6,A40,A41,Th20;
    end;
A42:   for k st k in dom v & v.k = i holds k<=m
    proof let k; assume
     A43: k in dom v & v.k=i;
     then f/.k in rng Col(G,i) by A16,A17;
     hence thesis by A7,A16,A19,A43;
    end;
  then A44: m+1 in dom v & v.(m+1)=i+1 by A3,A4,A5,A16,A19,A21,A22,A23,A27,A39,
Th14;
  thus m+1 in dom f by A3,A4,A5,A16,A19,A21,A22,A23,A27,A39,A42,Th14;
  thus thesis by A16,A17,A44;
 end;

theorem Th49:
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 & f/.1 in rng Col(G,1) and
  A2: f/.len f in rng Col(G,width G) and
  A3: f is_sequence_on G;
  A4: 1 in dom f & len f in dom f & dom f = Seg len f
   by A1,FINSEQ_1:def 3,FINSEQ_3:27;
  defpred P[Nat] means 1<=$1 & $1<=width G implies
     ex k st k in dom f & f/.k in rng Col(G,$1);
  A5: P[0];
  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
     A8: 1<=k+1 & k+1<=width G;
     then A9: k+1 in Seg width G by FINSEQ_1:3;
      per cases;
      suppose A10: k=0;
       take i=1;
       thus i in dom f & f/.i in rng Col(G,k+1) by A1,A10,FINSEQ_3:27;
      suppose k<>0; then 0<k & k<=k+1 by NAT_1:19,29;
       then A11: 0+1<=k & k<=width G by A8,NAT_1:38;
       defpred R[Nat] means $1 in dom f & f/.$1 in rng Col(G,k);
       A12: ex i st R[i] by A7,A11;
       A13: for i holds R[i] implies i<=len f by FINSEQ_3:27;
       A14: k in Seg width G by A11,FINSEQ_1:3;
       consider m such that
       A15: R[m] & for i st R[i] holds i<=m from Max(A13,A12);
       take n = m+1;
       thus n in dom f & f/.n in rng Col(G,k+1) by A1,A2,A3,A9,A14,A15,Th48;
    end;
  thus
A16: for i holds P[i] from Ind(A5,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
   A17: 1<=i & i<=width G & 2<=len f; then consider k such that
    A18: k in dom f & f/.k in rng Col(G,i) by A16;
      f/.k in L~f by A17,A18,Th16;
    then L~f /\ rng Col(G,i) <> {} by A18,XBOOLE_0:def 3;
    hence thesis by XBOOLE_0:def 7;
   end;
  let m,k,i,j; assume
  A19: 1<=m & m<=width G & 1<=k & k<=width G & i in dom f & j in dom f &
      f/.i in rng Col(G,m) &
      (for n st n in dom f & f/.n in rng Col(G,m) holds n<=i) & i<j &
      f/.j in rng Col(G,k);
  then A20: 1<=i & i<=len f & 1<=j & j<=len f by FINSEQ_3:27;
     now per cases;
   case m = width G; then len f<=i by A2,A4,A19;
    hence contradiction by A19,A20,AXIOMS:21;
   case m <> width G; then m<width G by A19,REAL_1:def 5;
    then 1<=m+1 & m+1<=width G by NAT_1:29,38;
    then m+1 in Seg width G & m in Seg width G by A19,FINSEQ_1:3;
    then A21: i+1 in dom f & f/.(i+1) in rng Col(G,m+1) & m+1 in Seg width G
     by A1,A2,A3,A19,Th48;
    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;
    A22: P[0];
    A23: for o be Nat st P[o] holds P[o+1]
     proof let o be Nat such that
      A24: P[o]; let n,l be Nat such that
      A25: n=o+1 & n>0 & i+n in dom f &
      f/.(i+n) in rng Col(G,l) & l in Seg width G;
         now per cases;
       suppose o=0;
        then l=m+1 & m<m+1 by A21,A25,Th20,NAT_1:38;
        hence m<l;
       suppose o<>0;
        then A26: 0<o by NAT_1:19;
        A27: 1<=i & i+n<=len f & i+n = i+o+1 & i+o<=i+o+1 & i<=i+o
          by A19,A25,FINSEQ_3:27,NAT_1:37,XCMPLX_1:1;
        then 1<=i+o & i+o<=len f by AXIOMS:22;
        then A28: i+o in dom f by FINSEQ_3:27;
        then consider l1 be Nat such that
        A29: l1 in Seg width G & f/.(i+o) in rng Col(G,l1) by A3,Th46;
        A30: m<l1 by A24,A26,A28,A29;
           now per cases by A3,A25,A27,A28,A29,Th47;
         suppose f/.(i+n) in rng Col(G,l1);
          hence m<l by A25,A29,A30,Th20;
         suppose for k st f/.(i+n) in rng Col(G,k) & k in Seg width G
              holds abs(l1-k) = 1;
then A31:          abs(l1-l) = 1 by A25;
             now per cases by A31,Th1;
           suppose l1>l & l1=l+1;
then A32:            m<=l by A30,NAT_1:38;
               now per cases by A32,REAL_1:def 5;
             case m=l;
              then i+n<=i by A19,A25;
              then n<=i-i by REAL_1:84;
              hence contradiction by A25,XCMPLX_1:14;
             case m<l;
              hence thesis;
             end;
            hence thesis;
           suppose l1<l & l=l1+1;
            hence thesis by A30,AXIOMS:22;
           end;
          hence thesis;
         end;
        hence thesis;
       end;
      hence thesis;
     end;
    A33: for o be Nat holds P[o] from Ind(A22,A23);
    A34: 0< j - i & i<=j by A19,SQUARE_1:11;
    reconsider l = j - i as Nat by A19,INT_1:18;
      i+l = j & k in Seg width G by A19,FINSEQ_1:3,XCMPLX_1:27;
    hence m<k by A19,A33,A34;
   end;
  hence thesis;
 end;

theorem Th50:
n in dom f & f/.n in rng Col(G,k) &
 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
  A1: n in dom f & f/.n in rng Col(G,k) &
   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;
A2: dom G = Seg len G & dom Col(G,k) = Seg len Col(G,k) by FINSEQ_1:def 3;
  A3: dom f = Seg len f by FINSEQ_1:def 3;
    0<width G by Lm1;
  then 0+1<=width G by NAT_1:38;
  then A4: 1 in Seg width G & 1<=k & k<=width G &
   1<=n & n<=len f by A1,A3,FINSEQ_1:3;
  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: P[0] by FINSEQ_3:27;
  A6: for i st P[i] holds P[i+1]
   proof let i such that
    A7: P[i]; assume
    A8: i+1 in dom f & i+1<=n;
    let m such that
    A9: m in Seg width G & f/.(i+1) in rng Col(G,m);
       now per cases;
     suppose i=0;
      hence thesis by A1,A4,A9,Th20;
     suppose i<>0;
      then 0<i & i<=i+1 & i<i+1 & i+1<=len f by A8,FINSEQ_3:27,NAT_1:19,38;
      then A10: 0+1<=i & i<=len f & i<=n & i<n by A8,NAT_1:38;
      then A11: i in dom f by FINSEQ_3:27;
      then consider i1,i2 be Nat such that
      A12: [i1,i2] in Indices G & f/.i = G*(i1,i2) by A1,Def11;
        Indices G = [:dom G,Seg width G:] by MATRIX_1:def 5;
      then A13: i1 in dom G & i2 in Seg width G &
       dom Col(G,i2) = Seg len Col(G,i2) &
      len Col(G,i2)=len G by A12,FINSEQ_1:def 3,MATRIX_1:def 9,ZFMISC_1:106;
      then Col(G,i2).i1 = f/.i by A12,MATRIX_1:def 9;
      then A14: f/.i in rng Col(G,i2) by A2,A13,FUNCT_1:def 5;
      then A15: i2<=k by A7,A10,A13,FINSEQ_3:27;
         now per cases by A15,REAL_1:def 5;
       case A16: i2<k;
           now per cases by A1,A8,A11,A13,A14,Th47;
         suppose f/.(i+1) in rng Col(G,i2); hence thesis by A9,A13,A16,Th20;
         suppose
             for j st f/.(i+1) in rng Col(G,j) &
           j in Seg width G holds abs(i2-j)=1;
          then A17: abs(i2-m)=1 by A9;
             now per cases by A17,Th1;
           suppose i2>m & i2=m+1; hence thesis by A16,AXIOMS:22;
           suppose i2<m & m=i2+1; hence thesis by A16,NAT_1:38;
           end;
          hence thesis;
         end;
        hence thesis;
       case i2=k; hence contradiction by A1,A10,A11,A14;
       end;
      hence thesis;
     end;
    hence thesis;
   end;
  thus for n holds P[n] from Ind(A5,A6);
 end;

theorem
  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
  A1: 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;
  then consider k such that
  A2: width G=k+1 & k>0 by Th3;
  A3: 0+1<=k by A2,NAT_1:38;
  A4: width G in Seg width G & dom f=dom f by A1,FINSEQ_1:3;
  then A5: len D=len G by A1,Def10;
  A6: Indices G = [:dom G,Seg width G:] by MATRIX_1:def 5;
A7: dom G = Seg len G & dom D = Seg len D & dom f = Seg len f
      by FINSEQ_1:def 3;
  defpred P[Nat] means $1 in dom f & f/.$1 in rng Col(G,k);
  A8: ex m st P[m]
   proof
      k<=k+1 by NAT_1:29;
    hence thesis by A1,A2,A3,Th49;
   end;
  consider m such that
  A9: P[m] & for i st P[i] holds m<=i from Min(A8);
  take t = f|m;
  A10: t = f|Seg m by TOPREAL1:def 1;
  A11: width D = k by A2,A4,Th26;
  then 1<width G & width D<width G by A2,A3,NAT_1:38;
  then A12: Col(D,1)=Col(G,1) & Col(D,width D)=Col(G,width D)
           by A2,A3,A4,A11,Th29;
  A13: 1<=m & m<=len f by A9,FINSEQ_3:27;
  then A14: len t = m & dom t=Seg len t by FINSEQ_1:def 3,TOPREAL1:3;
  then 1 in Seg m & len t in Seg m by A13,FINSEQ_1:3;
  hence t/.1 in rng Col(D,1) & t/.len t in rng Col(D,width D) & 1<=len t
   by A1,A9,A11,A12,A14,Th10,FINSEQ_1:3;
  A15: Indices D = [:dom D,Seg width D:] by MATRIX_1:def 5;
  A16: now let n; assume A17: n in dom t;
    then A18: n in dom f & t/.n=f/.n & n<=m by A9,A14,Th10,FINSEQ_3:27;
    then consider i,j such that
    A19: [i,j] in Indices G & f/.n=G*(i,j) by A1,Def11;
    take i,j;
    A20: i in dom G & j in Seg width G & len Col(G,j) = len G &
       dom Col(G,j)=Seg len Col(G,j) &
       for i st i in dom G holds Col(G,j).i=G*(i,j)
         by A6,A19,FINSEQ_1:def 3,MATRIX_1:def 9,ZFMISC_1:106;
    then Col(G,j).i=G*(i,j);
    then A21: 1<=j & f/.n in rng Col(G,j) by A7,A19,A20,FINSEQ_1:3,FUNCT_1:def
5;
      k<=k+1 by NAT_1:29;
    then k in Seg width G by A2,A3,FINSEQ_1:3;
    then j<=k by A1,A9,A18,A20,A21,Th50;
    then A22: j in Seg k by A21,FINSEQ_1:3;
    hence [i,j] in Indices D by A5,A7,A11,A15,A20,ZFMISC_1:106;
    thus t/.n = G*(i,j) by A9,A14,A17,A19,Th10
    .= D*(i,j) by A2,A20,A22,Th36;
   end;
     now let n; assume n in dom t & n+1 in dom t;
    then A23: t/.n=f/.n & t/.(n+1)=f/.(n+1) &
    n in dom f & n+1 in dom f by A9,A14,Th10;
    let i1,i2,j1,j2 be Nat; assume
    A24: [i1,i2] in Indices D & [j1,j2] in Indices D & t/.n=D*(i1,i2) &
               t/.(n+1)=D*(j1,j2);
    then A25: i1 in dom D & i2 in Seg k & j1 in dom D & j2 in Seg k
              by A11,A15,ZFMISC_1:106;
    then A26: f/.n=G*(i1,i2) & f/.(n+1)=G*(j1,j2) by A2,A5,A7,A23,A24,Th36;
      k<=k+1 by NAT_1:29;
    then Seg k c= Seg width G by A2,FINSEQ_1:7;
    then [i1,i2] in Indices G & [j1,j2] in Indices G by A5,A6,A7,A25,ZFMISC_1:
106;
    hence abs(i1-j1)+abs(i2-j2) = 1 by A1,A23,A26,Def11;
   end;
  hence t is_sequence_on D by A16,Def11;
  thus rng t c= rng f by A10,FUNCT_1:76;
 end;

theorem
  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
  A1: f is_sequence_on G & rng f /\ rng Col(G,1)<>{} &
      rng f /\ rng Col(G,width G)<>{};
  consider x being Element of rng f /\ rng Col(G,1);
  A2: x in rng f & x in rng Col(G,1) by A1,XBOOLE_0:def 3;
  then consider n such that
  A3: n in dom f & x=f/.n by PARTFUN2:4;
  consider y being Element of rng f /\ rng Col(G,width G);
  A4: y in rng f & y in rng Col(G,width G) by A1,XBOOLE_0:def 3;
  then consider m such that
  A5: m in dom f & y=f/.m by PARTFUN2:4;
  reconsider x as Point of TOP-REAL 2 by A3;
  A6: 1<=n & n<=len f & 1<=m & m<=len f by A3,A5,FINSEQ_3:27;
   per cases by AXIOMS:21;
   suppose A7: n=m;
    reconsider h = <*x*> as FinSequence of TOP-REAL 2;
    A8: len h=1 by FINSEQ_1:56;
    A9:
     now let k;
      assume
A10:      k in Seg 1;
       then A11:      k = 1 by FINSEQ_1:4,TARSKI:def 1;
         k in dom h by A10,FINSEQ_1:def 8;
      hence h/.k = h.k by FINSEQ_4:def 4 .= x by A11,FINSEQ_1:57;
     end;
    A12: rng h c= rng f
     proof let z be set; assume z in rng h;
      then consider i such that
A13:       i in dom h & z=h/.i by PARTFUN2:4;
          i in Seg 1 by A13,FINSEQ_1:def 8;
      hence thesis by A2,A9,A13;
     end;
    reconsider h as FinSequence of TOP-REAL 2;
    take h;
    thus rng h c= rng f by A12;
A14:  1 in Seg 1 by FINSEQ_1:3;
    then A15: h/.1=x & h/.len h=x & dom h=Seg len h by A8,A9,FINSEQ_1:def 3;
    thus h/.1 in rng Col(G,1) & h/.len h in rng Col(G,width G)
     by A2,A3,A4,A5,A7,A8,A9,A14;
    A16: now let i such that A17: i in dom h;
      consider i1,i2 be Nat such that
      A18: [i1,i2] in Indices G & f/.n=G*(i1,i2) by A1,A3,Def11;
      take i1,i2;
      thus [i1,i2] in Indices G & h/.i=G*(i1,i2) by A3,A8,A9,A15,A17,A18;
     end;
       now let i; assume i in dom h & i+1 in dom h;
     then i=1 & i+1=1 by A8,A15,FINSEQ_1:4,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 abs(i1-j1)+abs(i2-j2)=1;
     end;
    hence 1<=len h & h is_sequence_on G by A16,Def11,FINSEQ_1:56;
   suppose A19: n>m;
    set f1=f|n;
       m<=n & n<=n+1 by A19,NAT_1:29;
     then m<=n+1 by AXIOMS:22;
    then reconsider l=n+1-m as Nat by INT_1:18;
    A20: n+1-l=m by XCMPLX_1:18;
A21: now let i; assume i in Seg l;
      then A22: 1<=i & i<=l & 0<=m by FINSEQ_1:3,NAT_1:18;
      then l<=n+1-0 by REAL_1:92;
      then i<=n+1 by A22,AXIOMS:22;
     hence n+1-i is Nat by INT_1:18;
     end;
    A23: for i st i in Seg l holds n+1-i is Nat & f1/.(n+1-i)=f/.(n+1-i) &
      n+1-i in dom f
     proof let i; assume i in Seg l;
      then A24: 1<=i & i<=l & 0<=m by FINSEQ_1:3,NAT_1:18;
      then l<=n+1-0 by REAL_1:92;
      then i<=n+1 by A24,AXIOMS:22;
      then reconsider w=n+1-i as Nat by INT_1:18;
        n+1-i<=n+1-1 & n+1-l<=n+1-i by A24,REAL_1:92;
      then A25: n+1-i<=n & m<=n+1-i by XCMPLX_1:18,26;
      then 1<=n+1-i by A6,AXIOMS:22;
      then w in Seg n by A25,FINSEQ_1:3;
      hence thesis by A3,Th10;
     end;
    defpred P[Nat,set] means for k st $1+k = n+1 holds $2 = f1/.k;
    A26: for i st i in Seg l ex p st P[i,p]
     proof let i; assume
        i in Seg l;
      then reconsider a=n+1-i as Nat by A21;
      take f1/.a;
      let k;
      assume i+k = n+1;
      hence thesis by XCMPLX_1:26;
     end;
    consider g such that
    A27: len g = l & for i st i in Seg l holds P[i,g/.i]
         from FinSeqDChoice(A26);
    A28: dom g = Seg len g by FINSEQ_1:def 3;
    take g;
    thus rng g c= rng f
     proof let z be set; assume z in rng g;
      then consider i such that
      A29: i in dom g & z=g/.i by PARTFUN2:4;
      reconsider yy = n+1-i as Nat by A21,A27,A28,A29;
        i + yy = n+1 by XCMPLX_1:27;
      then z=f1/.yy & f1/.yy=f/.yy & yy in dom f
        by A23,A27,A28,A29;
      hence z in rng f by PARTFUN2:4;
     end;
      m+1<=n & n<=n+1 by A19,NAT_1:38;
    then A30: m+1<=n+1 & dom g=Seg len g by AXIOMS:22,FINSEQ_1:def 3;
     then m <= n & 1<=l & len g=l by A27,REAL_1:53,84;
    then A31:1 in Seg l & m in Seg n & len g in dom g & n in Seg n
     by A6,FINSEQ_1:3,FINSEQ_3:27;
    then g/.1 = f1/.n by A27
     .= f/.n by A3,A31,Th10;
    hence g/.1 in rng Col(G,1) by A1,A3,XBOOLE_0:def 3;
      len g <> 0 by A27,A30,REAL_1:84;
    then l in dom g by A27,A30,FINSEQ_1:5;
    then reconsider ww = n+1-l as Nat by A21,A27,A30;
      l + ww = n+1 by XCMPLX_1:27;
    then g/.len g= f1/.ww by A27,A28,A31
    .= f/.m by A3,A20,A31,Th10;
    hence g/.len g in rng Col(G,width G) by A1,A5,XBOOLE_0:def 3;
    A32: now let i; assume A33: i in dom g;
      then reconsider ww=n+1-i as Nat by A21,A27,A30;
      i + ww = n+1 by XCMPLX_1:27;
then A34: i in Seg l & dom g=Seg l & g/.i=f1/.ww by A27,A28,A33;
       then ww in dom f & g/.i=f/.ww by A23;
      then consider i1,i2 be Nat such that
      A35: [i1,i2] in Indices G & f/.ww=G*(i1,i2) by A1,Def11;
      take i1,i2;
      thus [i1,i2] in Indices G & g/.i=G*(i1,i2) by A23,A34,A35;
     end;
       now let i; assume
A36:  i in dom g & i+1 in dom g;
      then reconsider ww = n+1-i as Nat by A21,A27,A30;
      reconsider xx = n+1-(i+1) as Nat by A21,A27,A30,A36;
     i + ww = n+1 & i+1 + xx = n+1 by XCMPLX_1:27;
      then A37: i in Seg l & i+1 in Seg l & dom g=Seg l & g/.i=f1/.ww &
      g/.(i+1)=f1/.xx & n+1-(i+1)=n+1-i-1 by A27,A28,A36,XCMPLX_1:36;
      then A38: ww in dom f & g/.i=f/.ww &
      xx in dom f & g/.(i+1)=f/.xx by A23;
      A39: xx+1=n+1-i by A37,XCMPLX_1:27;
      let i1,i2,j1,j2 be Nat; assume
        [i1,i2] in Indices G & [j1,j2] in Indices G & g/.i=G*(i1,i2) &
      g/.(i+1)=G*(j1,j2);
      hence 1=abs(j1-i1)+abs(j2-i2) by A1,A38,A39,Def11
      .= abs(-(i1-j1))+abs(j2-i2) by XCMPLX_1:143
      .= abs(-(i1-j1))+abs(-(i2-j2)) by XCMPLX_1:143
      .= abs(i1-j1)+abs(-(i2-j2)) by ABSVALUE:17
      .= abs(i1-j1)+abs(i2-j2) by ABSVALUE:17;
     end;
    hence 1<=len g & g is_sequence_on G by A27,A30,A32,Def11,REAL_1:84;
   suppose A40: n<m;
    set f1=f|m;
       n<=m & m<=m+1 by A40,NAT_1:29;
    then n<=m+1 by AXIOMS:22;
    then reconsider l=m+1-n as Nat by INT_1:18;
     reconsider w=n-1 as Nat by A6,INT_1:18;
A41: for i st i in Seg l holds n-1 is Nat & f1/.(w+i)=f/.(w+i) &
     n-1+i in dom f
     proof let i; assume
         i in Seg l;
      then 0<=w & 1<=i & i<=l by FINSEQ_1:3,NAT_1:18;
      then A42: 0+1<=w+i & i+n<=l+n by REAL_1:55;
      then i+n<=m+1 by XCMPLX_1:27;
      then i+n-1<=m by REAL_1:86;
      then w+i<=m by XCMPLX_1:29;
      then w+i in Seg m by A42,FINSEQ_1:3;
      hence thesis by A5,Th10;
     end;
    defpred P[Nat,set] means $2=f1/.(w+$1);
    A43: for i st i in Seg l ex p st P[i,p];
    consider g such that
    A44: len g= l & for i st i in Seg l holds P[i,g/.i]
     from FinSeqDChoice(A43);
A45: dom g = Seg l by A44,FINSEQ_1:def 3;
    take g;
    A46: dom g = Seg len g by FINSEQ_1:def 3;
    thus rng g c= rng f
     proof let z be set; assume z in rng g;
      then consider i such that
      A47: i in dom g & z=g/.i by PARTFUN2:4;
        z=f1/.(w+i) & f1/.(w+i)=f/.(w+i) & w+i in dom f
        by A41,A44,A46,A47;
      hence z in rng f by PARTFUN2:4;
     end;
      n+1<=m & m<=m+1 by A40,NAT_1:38;
     then A48: n+1<=m+1 & dom g=Seg len g by AXIOMS:22,FINSEQ_1:def 3;
    then A49: n <= m & 1<=l & len g=l by A44,REAL_1:53,84;
    A50: w+l=w+(m-n+1) by XCMPLX_1:29
     .= w+(m-w) by XCMPLX_1:37
     .= m by XCMPLX_1:27;
    A51:1 in Seg l & n in Seg m & len g in dom g & m in Seg m
     by A6,A49,FINSEQ_1:3,FINSEQ_3:27;
    then g/.1 = f1/.(n-1+1) by A44
     .= f1/.n by XCMPLX_1:27
     .= f/.n by A5,A51,Th10;
    hence g/.1 in rng Col(G,1) by A1,A3,XBOOLE_0:def 3;
    reconsider ww = m+1-n as Nat by A44;
      g/.len g= f1/.(w+ww) by A44,A45,A51
    .= f/.m by A5,A50,A51,Th10;
    hence g/.len g in rng Col(G,width G) by A1,A5,XBOOLE_0:def 3;
    A52: now let i; assume i in dom g;
then A53:      i in Seg l & dom g=Seg l & g/.i=f1/.(w+i) by A44,A45;
       then w+i in dom f & g/.i=f/.(w+i) by A41;
      then consider i1,i2 be Nat such that
      A54: [i1,i2] in Indices G & f/.(w+i)=G*(i1,i2) by A1,Def11;
      take i1,i2;
      thus [i1,i2] in Indices G & g/.i=G*(i1,i2) by A41,A53,A54;
     end;
       now let i; assume
        i in dom g & i+1 in dom g;
then i in Seg l & i+1 in Seg l & dom g=Seg l & g/.i=f1/.(w+i) &
      g/.(i+1)=f1/.(w+(i+1)) & w+(i+1)=w+i+1 by A44,A45,XCMPLX_1:1;
      then A55: w+i in dom f & g/.i=f/.(w+i) &
      w+i+1 in dom f & g/.(i+1)=f/.(w+i+1) by A41;
      let i1,i2,j1,j2 be Nat; assume
         [i1,i2] in Indices G & [j1,j2] in Indices G & g/.i=G*(i1,i2) &
      g/.(i+1)=G*(j1,j2);
      hence abs(i1-j1)+abs(i2-j2)=1 by A1,A55,Def11;
     end;
    hence thesis by A44,A48,A52,Def11,REAL_1:84;
 end;

theorem
  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 ex j st j in dom f & n<=j &
 f/.j in rng Line(G,i)) &
for i st k<i & i<=len G 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 and
  A3: f/.len f in rng Line(G,len G) and
  A4: n in dom f and
  A5: f/.n in rng Line(G,k);
  A6: 1<=k & k<=len G & dom f=Seg len f by A1,FINSEQ_1:def 3,FINSEQ_3:27;
  A7: 1<=n & n<=len f by A4,FINSEQ_3:27;
  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);
  A8: P[0] by A6,AXIOMS:22;
  A9: for i st P[i] holds P[i+1]
   proof let i such that
    A10: P[i]; assume
    A11: k<=i+1 & i+1<=len G;
       now per cases by A11,REAL_1:def 5;
     suppose A12: k=i+1;
      take j=n;
      thus j in dom f & n<=j & f/.j in rng Line(G,i+1) by A4,A5,A12;
     suppose A13: k<i+1;
then k<=i & i<=i+1 & k<=i+1 by NAT_1:38;
       then 1<=i & i<=len G & 1<=i+1 & k<=i by A6,A11,AXIOMS:22;
      then A14: i in dom G & i+1 in dom G by A11,FINSEQ_3:27;
      defpred P[Nat] means $1 in dom f & n<=$1 & f/.$1 in rng Line(G,i);
A15: ex j st P[j] by A10,A11,A13,NAT_1:38;
      A16: for j st P[j] holds j<=len f by FINSEQ_3:27;
      consider ma be Nat such that
      A17: P[ma] & for j st P[j] holds j<=ma from Max(A16,A15);
      A18: 1<=len f by A7,AXIOMS:22;
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 A17,AXIOMS:22;
         suppose n<=j; hence j<=ma by A17,A20;
         end;
        hence j<=ma;
       end;
      take j=ma+1;
      thus j in dom f by A2,A3,A14,A17,A18,A19,Th44;
        ma<=ma+1 by NAT_1:29;
      hence n<=j & f/.j in rng Line(G,i+1)
       by A2,A3,A14,A17,A18,A19,Th44,AXIOMS:22;
     end;
    hence thesis;
   end;
  thus
A21: for i holds P[i] from Ind(A8,A9);
  let i; assume
  A22: k<i & i<=len G;
  then consider j such that
  A23: j in dom f & n<=j & f/.j in rng Line(G,i) by A21;
    1<=i by A6,A22,AXIOMS:22;
  then A24: i in dom G by A22,FINSEQ_3:27;
  take j;
  thus j in dom f by A23;
     n<>j by A1,A5,A22,A23,A24,Th19;
  hence thesis by A23,REAL_1:def 5;
 end;

Back to top