The Mizar article:

Some Properties of Cells on Go Board

by
Czeslaw Bylinski

Received April 23, 1999

Copyright (c) 1999 Association of Mizar Users

MML identifier: GOBRD13
[ MML identifier index ]


environ

 vocabulary FINSEQ_1, FINSEQ_2, EUCLID, FUNCT_1, PROB_1, FUNCT_6, RELAT_1,
      MATRLIN, PRALG_1, TARSKI, FINSET_1, MATRIX_1, TREES_1, CARD_1, CARD_2,
      GOBOARD1, MCART_1, ARYTM_1, GOBOARD5, GOBOARD2, PRE_TOPC, BOOLE,
      TOPREAL1, ABSVALUE, RFINSEQ, GOBRD13, FINSEQ_4;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XREAL_0, REAL_1, NAT_1,
      BINARITH, ABSVALUE, STRUCT_0, RELAT_1, FUNCT_1, FUNCT_2, CARD_1, CARD_2,
      FINSEQ_1, FINSEQ_2, MATRLIN, PRALG_1, FINSEQ_4, FINSET_1, PROB_1,
      FUNCT_6, RFINSEQ, MATRIX_1, PRE_TOPC, EUCLID, TOPREAL1, GOBOARD1,
      GOBOARD2, GOBOARD5;
 constructors REAL_1, ABSVALUE, RFINSEQ, SEQM_3, BINARITH, CARD_2, GOBOARD2,
      GOBOARD5, PRALG_1, MATRLIN, WELLORD2, PROB_1, MEMBERED;
 clusters STRUCT_0, RELSET_1, EUCLID, GOBOARD2, GOBOARD5, FINSEQ_1, CARD_1,
      MEMBERED, NUMBERS, ORDINAL2;
 requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
 definitions TARSKI, PRALG_1, MATRLIN;
 theorems ZFMISC_1, NAT_1, FINSEQ_1, MATRIX_1, GOBOARD1, EUCLID, FINSEQ_3,
      AXIOMS, REAL_1, TARSKI, JORDAN3, FINSEQ_5, GOBOARD7, TOPREAL1, BINARITH,
      AMI_5, RLVECT_1, GOBOARD5, ABSVALUE, FUNCT_1, GOBOARD9, FINSEQ_2, PROB_1,
      GOBRD11, GOBOARD2, SPRECT_3, JORDAN5D, CARD_2, CARD_4, FINSET_1,
      YELLOW_6, FUNCT_6, RFINSEQ, JORDAN8, EXTENS_1, MATRLIN, CARD_1, PRE_CIRC,
      PARTFUN2, XCMPLX_1;
 schemes FRAENKEL;

begin

 reserve i,i1,i2,i',i1',j,j1,j2,j',j1',k,k1,k2,l,m,n for Nat;
 reserve r,s,r',s' for Real;
 reserve D for non empty set, f for FinSequence of D;

definition let E be non empty set;
  let S be FinSequence-DOMAIN of the carrier of TOP-REAL 2;
  let F be Function of E,S; let e be Element of E;
 redefine func F.e -> FinSequence of TOP-REAL 2;
coherence
 proof
   thus F.e is FinSequence of TOP-REAL 2 by FINSEQ_2:def 3;
 end;
end;

definition let F be Function;
   func Values F -> set equals
:Def1: Union rngs F;
 correctness;
end;

theorem Th1:
   for M being FinSequence of D* holds M.i is FinSequence of D
proof let M be FinSequence of D*;
 per cases;
 suppose not i in dom M;
   then M.i = <*>D by FUNCT_1:def 4;
  hence thesis;
 suppose i in dom M;
then A1: M.i in rng M by FUNCT_1:def 5;
    rng M c= D* by FINSEQ_1:def 4;
  hence thesis by A1,FINSEQ_1:def 11;
end;

definition
 let D be set;
 cluster -> FinSequence-yielding FinSequence of D*;
 coherence proof let f be FinSequence of D*;
  let x be set; assume x in dom f; then f.x in D* by FINSEQ_2:13;
  hence f.x is FinSequence by FINSEQ_1:def 11;
 end;
end;

definition
 cluster FinSequence-yielding -> Function-yielding Function;
 coherence proof let f be Function; assume
 A1: f is FinSequence-yielding;
  let x be set;
  thus thesis by A1,MATRLIN:def 1;
 end;
end;

canceled;

theorem Th3:
  for M being FinSequence of D*
   holds Values M = union {rng f where f is Element of D*: f in rng M}
proof let M be FinSequence of D*;
  set R = {rng f where f is Element of D*: f in rng M};
A1: Values M = Union rngs M by Def1;
A2: Union rngs M = union rng rngs M by PROB_1:def 3;
   now let y be set;
  hereby assume y in Values M;
   then consider Y being set such that
A3:  y in Y and
A4:  Y in rng rngs M by A1,A2,TARSKI:def 4;
   consider i being set such that
A5:  i in dom rngs M and
A6:  (rngs M).i = Y by A4,FUNCT_1:def 5;
A7:  i in dom M by A5,EXTENS_1:4;
   then reconsider i as Nat;
   reconsider f = M.i as FinSequence of D by Th1;
     f in rng M & f in D* by A7,FINSEQ_1:def 11,FUNCT_1:def 5;
then A8:  rng f in R;
     Y = rng f by A6,A7,FUNCT_6:31;
   hence y in union R by A3,A8,TARSKI:def 4;
  end;
  assume y in union R;
  then consider Y being set such that
A9:  y in Y and
A10:  Y in R by TARSKI:def 4;
  consider f being Element of D* such that
A11:  Y = rng f and
A12:  f in rng M by A10;
  consider i such that
A13:  i in dom M and
A14:  M.i = f by A12,FINSEQ_2:11;
    i in dom rngs M & (rngs M).i = rng f by A13,A14,FUNCT_6:31;
  then rng f in rng rngs M by FUNCT_1:def 5;
  hence y in Values M by A1,A2,A9,A11,TARSKI:def 4;
 end;
 hence thesis by TARSKI:2;
end;

definition let D be non empty set, M be FinSequence of D*;
  cluster Values M -> finite;
 coherence
  proof
    deffunc F(Function) = rng $1;
    set A = {F(f) where f is Element of D*: f in rng M};
A1:  rng M is finite;
A2:  {F(f) where f is Element of D*: f in rng M} is finite
       from FraenkelFin(A1);
     now let X be set;
    assume X in A;
    then ex f being Element of D* st X = rng f & f in rng M;
    hence X is finite;
   end;
   then union A is finite by A2,FINSET_1:25;
   hence thesis by Th3;
  end;
end;

theorem Th4:
  for M being Matrix of D st i in dom M & M.i = f holds len f = width M
proof let M be Matrix of D such that
A1:  i in dom M and
A2:  M.i = f;
A3:  M.i in rng M by A1,FUNCT_1:def 5;
    M is non empty by A1,FINSEQ_1:26;
  then len M <> 0 by FINSEQ_1:25;
  then len M > 0 by NAT_1:19;
  then consider p being FinSequence such that
A4:  p in rng M and
A5:  len p = width M by MATRIX_1:def 4;
  consider n being Nat such that
A6:  for x being set st x in rng M ex s being FinSequence st s=x & len s = n
    by MATRIX_1:def 1;
A7: ex s being FinSequence st s = p & len s = n by A4,A6;
    ex s being FinSequence st s = M.i & len s = n by A3,A6;
  hence thesis by A2,A5,A7;
end;

theorem Th5:
  for M being Matrix of D st i in dom M & M.i = f & j in dom f
   holds [i,j] in Indices M
 proof let M be Matrix of D such that
A1:  i in dom M and
A2:  M.i = f and
A3:  j in dom f;
A4:  M.i in rng M by A1,FUNCT_1:def 5;
    M is non empty by A1,FINSEQ_1:26;
  then len M <> 0 by FINSEQ_1:25;
  then len M > 0 by NAT_1:19;
  then consider p being FinSequence such that
A5:  p in rng M and
A6:  len p = width M by MATRIX_1:def 4;
  consider n being Nat such that
A7:  for x being set st x in rng M ex s being FinSequence st s=x & len s = n
    by MATRIX_1:def 1;
A8: ex s being FinSequence st s = p & len s = n by A5,A7;
A9: Indices M = [:dom M,Seg width M:] by MATRIX_1:def 5;
    ex s being FinSequence st s = M.i & len s = n by A4,A7;
  then j in Seg width M by A2,A3,A6,A8,FINSEQ_1:def 3;
  hence thesis by A1,A9,ZFMISC_1:106;
 end;

theorem Th6:
 for M being Matrix of D st [i,j] in Indices M & M.i = f
  holds len f = width M & j in dom f
proof let M be Matrix of D such that
A1:  [i,j] in Indices M;
A2:  Indices M = [:dom M,Seg width M:] by MATRIX_1:def 5;
then A3:  i in dom M by A1,ZFMISC_1:106;
then A4:  M.i in rng M by FUNCT_1:def 5;
A5:  j in Seg width M by A1,A2,ZFMISC_1:106;
    M is non empty by A3,FINSEQ_1:26;
  then len M <> 0 by FINSEQ_1:25;
  then len M > 0 by NAT_1:19;
  then consider p being FinSequence such that
A6:  p in rng M and
A7:  len p = width M by MATRIX_1:def 4;
  consider n being Nat such that
A8:  for x being set st x in rng M ex s being FinSequence st s=x & len s = n
    by MATRIX_1:def 1;
A9: ex s being FinSequence st s = p & len s = n by A6,A8;
    ex s being FinSequence st s = M.i & len s = n by A4,A8;
  hence thesis by A5,A7,A9,FINSEQ_1:def 3;
end;

theorem Th7:
 for M being Matrix of D holds Values M = { M*(i,j): [i,j] in Indices M }
proof let M be Matrix of D;
 set V = { M*(i,j): [i,j] in Indices M },
     R = {rng f where f is Element of D*: f in rng M};
A1: Values M = union R by Th3;
   now let y be set;
  hereby assume y in Values M;
   then consider Y being set such that
A2:  y in Y and
A3:  Y in R by A1,TARSKI:def 4;
   consider f being Element of D* such that
A4:  Y = rng f and
A5:  f in rng M by A3;
   consider i such that
A6:  i in dom M and
A7:  M.i = f by A5,FINSEQ_2:11;
   consider j such that
A8:  j in dom f and
A9:  f.j = y by A2,A4,FINSEQ_2:11;
A10:  [i,j] in Indices M by A6,A7,A8,Th5;
   then ex p being FinSequence of D st p = M.i & M*(i,j) = p.j by MATRIX_1:def
6;
   hence y in V by A7,A9,A10;
  end;
  assume y in V;
  then consider i,j such that
A11:  y = M*(i,j) and
A12:  [i,j] in Indices M;
  consider f being FinSequence of D such that
A13:  f = M.i and
A14:  M*(i,j) = f.j by A12,MATRIX_1:def 6;
     Indices M = [:dom M,Seg width M:] by MATRIX_1:def 5;
   then i in dom M by A12,ZFMISC_1:106;
then A15:  M.i in rng M by FUNCT_1:def 5;
    f in D* by FINSEQ_1:def 11;
then A16:  rng f in R by A13,A15;
    j in dom f by A12,A13,Th6;
  then f.j in rng f by FUNCT_1:def 5;
  hence y in Values M by A1,A11,A14,A16,TARSKI:def 4;
 end;
 hence thesis by TARSKI:2;
end;

theorem
    for D being non empty set, M being Matrix of D holds
    card Values M <= (len M)*(width M)
proof let D be non empty set, M be Matrix of D;
A1:  Card dom rngs M = Card dom M by EXTENS_1:4
                    .= Card M by PRE_CIRC:21
                    .= Card len M by CARD_1:def 5;
    now let x be set;
   assume x in dom rngs M;
then A2:  x in dom M by EXTENS_1:4;
   then reconsider i = x as Nat;
   reconsider f = M.i as FinSequence of D by Th1;
     Card rng f c= Card dom f by YELLOW_6:3;
   then Card rng f c= Card Seg len f by FINSEQ_1:def 3;
   then Card rng f c= Card len f by FINSEQ_1:76;
   then Card rng f c= Card width M by A2,Th4;
   hence Card ((rngs M).x) c= Card width M by A2,FUNCT_6:31;
  end;
 then Card Union rngs M c= Card(len M)*`Card(width M) by A1,CARD_4:59;
 then Card Values M c= Card(len M)*`Card(width M) by Def1;
 then Card Values M c= Card((len M)*(width M)) by CARD_2:52;
 then card Values M <= card((len M)*(width M)) by CARD_2:57;
 hence card Values M <= (len M)*(width M) by FINSEQ_1:78;
end;

reserve f for FinSequence of TOP-REAL 2, G for Go-board;

theorem
    for G being Matrix of TOP-REAL 2 holds
  f is_sequence_on G implies rng f c= Values G
proof
  let G be Matrix of TOP-REAL 2;
assume
A1: f is_sequence_on G;
  let y be set;
  assume y in rng f;
  then consider n such that
A2:  n in dom f and
A3:  f/.n = y by PARTFUN2:4;
    ex i,j st [i,j] in Indices G & f/.n = G*(i,j) by A1,A2,GOBOARD1:def 11;
  then y in { G*(i,j): [i,j] in Indices G } by A3;
  hence thesis by Th7;
end;

theorem Th10:
   for G1,G2 being Go-board
    st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 &
       G1*(i1,j1) = G2*(1,j2)
   holds i1 = 1
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  1 <= j2 & j2 <= width G2 and
A4:  G1*(i1,j1) = G2*(1,j2);
A5:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
     0 <> len G2 by GOBOARD1:def 5;
then A6: 1 <= len G2 by RLVECT_1:99;
     0 <> len G1 by GOBOARD1:def 5;
then A7: 1 <= len G1 by RLVECT_1:99;
 set p = G1*(1,j1);
 assume i1 <> 1;
 then 1 < i1 by A5,REAL_1:def 5;
then A8: p`1 < G1*(i1,j1)`1 by A5,GOBOARD5:4;
   [1,j1] in Indices G1 by A5,A7,GOBOARD7:10;
 then p in {G1*(i,j): [i,j] in Indices G1};
 then p in Values G1 by Th7;
 then p in Values G2 by A1;
 then p in {G2*(i,j): [i,j] in Indices G2} by Th7;
 then consider i,j such that
A9:  p = G2*(i,j) and
A10:  [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A10,GOBOARD5:1;
then A12:  G2*(1,j)`1 = G2*(1,1)`1 by A6,GOBOARD5:3
               .= G2*(1,j2)`1 by A3,A6,GOBOARD5:3;
  then 1 < i by A4,A8,A9,A11,REAL_1:def 5;
  hence contradiction by A4,A8,A9,A11,A12,GOBOARD5:4;
end;

theorem Th11:
   for G1,G2 being Go-board
    st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & 1 <= j2 & j2 <= width G2 &
       G1*(i1,j1) = G2*(len G2,j2)
   holds i1 = len G1
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  1 <= j2 & j2 <= width G2 and
A4:  G1*(i1,j1) = G2*(len G2,j2);
A5:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
     0 <> len G2 by GOBOARD1:def 5;
then A6: 1 <= len G2 by RLVECT_1:99;
     0 <> len G1 by GOBOARD1:def 5;
then A7: 1 <= len G1 by RLVECT_1:99;
 set p = G1*(len G1,j1);
 assume i1 <> len G1;
 then i1 < len G1 by A5,REAL_1:def 5;
then A8:  G1*(i1,j1)`1 < p`1 by A5,GOBOARD5:4;
   [len G1,j1] in Indices G1 by A5,A7,GOBOARD7:10;
 then p in {G1*(i,j): [i,j] in Indices G1};
 then p in Values G1 by Th7;
 then p in Values G2 by A1;
 then p in {G2*(i,j): [i,j] in Indices G2} by Th7;
 then consider i,j such that
A9:  p = G2*(i,j) and
A10:  [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A10,GOBOARD5:1;
then A12:  G2*(len G2,j)`1 = G2*(len G2,1)`1 by A6,GOBOARD5:3
                   .= G2*(len G2,j2)`1 by A3,A6,GOBOARD5:3;
  then i < len G2 by A4,A8,A9,A11,REAL_1:def 5;
  hence contradiction by A4,A8,A9,A11,A12,GOBOARD5:4;
end;

theorem Th12:
   for G1,G2 being Go-board
    st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 &
       G1*(i1,j1) = G2*(i2,1)
   holds j1 = 1
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  1 <= i2 & i2 <= len G2 and
A4:  G1*(i1,j1) = G2*(i2,1);
A5:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
     0 <> width G2 by GOBOARD1:def 5;
then A6: 1 <= width G2 by RLVECT_1:99;
     0 <> width G1 by GOBOARD1:def 5;
then A7: 1 <= width G1 by RLVECT_1:99;
 set p = G1*(i1,1);
 assume j1 <> 1;
 then 1 < j1 by A5,REAL_1:def 5;
then A8:  p`2 < G1*(i1,j1)`2 by A5,GOBOARD5:5;
   [i1,1] in Indices G1 by A5,A7,GOBOARD7:10;
 then p in {G1*(i,j): [i,j] in Indices G1};
 then p in Values G1 by Th7;
 then p in Values G2 by A1;
 then p in {G2*(i,j): [i,j] in Indices G2} by Th7;
 then consider i,j such that
A9:  p = G2*(i,j) and
A10:  [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A10,GOBOARD5:1;
then A12:  G2*(i,1)`2 = G2*(1,1)`2 by A6,GOBOARD5:2
               .= G2*(i2,1)`2 by A3,A6,GOBOARD5:2;
  then 1 < j by A4,A8,A9,A11,REAL_1:def 5;
  hence contradiction by A4,A8,A9,A11,A12,GOBOARD5:5;
end;

theorem Th13:
   for G1,G2 being Go-board st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & 1 <= i2 & i2 <= len G2 &
       G1*(i1,j1) = G2*(i2,width G2)
   holds j1 = width G1
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  1 <= i2 & i2 <= len G2 and
A4:  G1*(i1,j1) = G2*(i2,width G2);
A5:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
     0 <> width G2 by GOBOARD1:def 5;
then A6: 1 <= width G2 by RLVECT_1:99;
     0 <> width G1 by GOBOARD1:def 5;
then A7: 1 <= width G1 by RLVECT_1:99;
 set p = G1*(i1,width G1);
 assume j1 <> width G1;
 then j1 < width G1 by A5,REAL_1:def 5;
then A8:  G1*(i1,j1)`2 < p`2 by A5,GOBOARD5:5;
   [i1,width G1] in Indices G1 by A5,A7,GOBOARD7:10;
 then p in {G1*(i,j): [i,j] in Indices G1};
 then p in Values G1 by Th7;
 then p in Values G2 by A1;
 then p in {G2*(i,j): [i,j] in Indices G2} by Th7;
 then consider i,j such that
A9:  p = G2*(i,j) and
A10:  [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A10,GOBOARD5:1;
then A12:  G2*(i,width G2)`2 = G2*(1,width G2)`2 by A6,GOBOARD5:2
                      .= G2*(i2,width G2)`2 by A3,A6,GOBOARD5:2;
  then j < width G2 by A4,A8,A9,A11,REAL_1:def 5;
  hence contradiction by A4,A8,A9,A11,A12,GOBOARD5:5;
end;

theorem Th14:
   for G1,G2 being Go-board st Values G1 c= Values G2 &
       1 <= i1 & i1 < len G1 & 1 <= j1 & j1 <= width G1 &
       1 <= i2 & i2 < len G2 & 1 <= j2 & j2 <= width G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds G2*(i2+1,j2)`1 <= G1*(i1+1,j1)`1
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  1 <= i1 & i1 < len G1 and
A3:  1 <= j1 & j1 <= width G1 and
A4:  1 <= i2 & i2 < len G2 and
A5:  1 <= j2 & j2 <= width G2 and
A6:  G1*(i1,j1) = G2*(i2,j2);
 set p = G1*(i1+1,j1);
 assume
A7:  p`1 < G2*(i2+1,j2)`1;
A8:  1 <= i1+1 & i1 < i1+1 & i1+1 <= len G1 by A2,NAT_1:38;
 then [i1+1,j1] in Indices G1 by A3,GOBOARD7:10;
 then p in {G1*(i,j): [i,j] in Indices G1};
 then p in Values G1 by Th7;
 then p in Values G2 by A1;
 then p in {G2*(i,j): [i,j] in Indices G2} by Th7;
 then consider i,j such that
A9:  p = G2*(i,j) and
A10:  [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A10,GOBOARD5:1;
then A12:  G2*(i,j)`1 = G2*(i,1)`1 by GOBOARD5:3
               .= G2*(i,j2)`1 by A5,A11,GOBOARD5:3;
then A13:  G2*(i2,j2)`1 < G2*(i,j2)`1 by A2,A3,A6,A8,A9,GOBOARD5:4;
A14: now assume i <= i2;
     then i = i2 or i < i2 by REAL_1:def 5;
     hence contradiction by A4,A5,A11,A13,GOBOARD5:4;
    end;
A15:  1 <= i2+1 & i2 < i2+1 & i2+1 <= len G2 by A4,NAT_1:38;
     now assume i2+1 <= i;
     then i2+1 = i or i2+1 < i by REAL_1:def 5;
     hence contradiction by A5,A7,A9,A11,A12,A15,GOBOARD5:4;
   end;
 hence contradiction by A14,NAT_1:38;
end;

theorem Th15:
   for G1,G2 being Go-board st G1*(i1-'1,j1) in Values G2 &
       1 < i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 &
       1 < i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds G1*(i1-'1,j1)`1 <= G2*(i2-'1,j2)`1
proof let G1,G2 be Go-board such that
A1:  G1*(i1-'1,j1) in Values G2 and
A2:  1 < i1 & i1 <= len G1 and
A3:  1 <= j1 & j1 <= width G1 and
A4:  1 < i2 & i2 <= len G2 and
A5:  1 <= j2 & j2 <= width G2 and
A6:  G1*(i1,j1) = G2*(i2,j2);
 set p = G1*(i1-'1,j1);
 assume
A7:  G2*(i2-'1,j2)`1 < p`1;
A8:  1 <= i1-'1 by A2,JORDAN3:12;
then A9:  i1-'1 < i1 by JORDAN3:14;
   p in {G2*(i,j): [i,j] in Indices G2} by A1,Th7;
 then consider i,j such that
A10:  p = G2*(i,j) and
A11:  [i,j] in Indices G2;
A12: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A11,GOBOARD5:1;
then A13:  G2*(i,j)`1 = G2*(i,1)`1 by GOBOARD5:3
               .= G2*(i,j2)`1 by A5,A12,GOBOARD5:3;
then A14:  G2*(i,j2)`1 < G2*(i2,j2)`1 by A2,A3,A6,A8,A9,A10,GOBOARD5:4;
A15: now assume i2 <= i;
     then i = i2 or i2 < i by REAL_1:def 5;
     hence contradiction by A4,A5,A12,A14,GOBOARD5:4;
    end;
    1 <= i2-'1 by A4,JORDAN3:12;
  then i2-'1 < i2 by JORDAN3:14;
then A16:  i2-'1 < len G2 by A4,AXIOMS:22;
     now assume i <= i2-'1;
     then i2-'1 = i or i < i2-'1 by REAL_1:def 5;
     hence contradiction by A5,A7,A10,A12,A13,A16,GOBOARD5:4;
   end;
 hence contradiction by A15,JORDAN3:12;
end;

theorem Th16:
   for G1,G2 being Go-board st G1*(i1,j1+1) in Values G2 &
       1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 < width G1 &
       1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 < width G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds G2*(i2,j2+1)`2 <= G1*(i1,j1+1)`2
proof let G1,G2 be Go-board such that
A1:  G1*(i1,j1+1) in Values G2 and
A2:  1 <= i1 & i1 <= len G1 and
A3:  1 <= j1 & j1 < width G1 and
A4:  1 <= i2 & i2 <= len G2 and
A5:  1 <= j2 & j2 < width G2 and
A6:  G1*(i1,j1) = G2*(i2,j2);
 set p = G1*(i1,j1+1);
 assume
A7:  p`2 < G2*(i2,j2+1)`2;
A8:  1 <= j1+1 & j1 < j1+1 & j1+1 <= width G1 by A3,NAT_1:38;
   p in {G2*(i,j): [i,j] in Indices G2} by A1,Th7;
 then consider i,j such that
A9:  p = G2*(i,j) and
A10:  [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A10,GOBOARD5:1;
then A12:  G2*(i,j)`2 = G2*(1,j)`2 by GOBOARD5:2
               .= G2*(i2,j)`2 by A4,A11,GOBOARD5:2;
then A13:  G2*(i2,j2)`2 < G2*(i2,j)`2 by A2,A3,A6,A8,A9,GOBOARD5:5;
A14: now assume j <= j2;
     then j = j2 or j < j2 by REAL_1:def 5;
     hence contradiction by A4,A5,A11,A13,GOBOARD5:5;
    end;
A15:  1 <= j2+1 & j2 < j2+1 & j2+1 <= width G2 by A5,NAT_1:38;
     now assume j2+1 <= j;
     then j2+1 = j or j2+1 < j by REAL_1:def 5;
     hence contradiction by A4,A7,A9,A11,A12,A15,GOBOARD5:5;
   end;
 hence contradiction by A14,NAT_1:38;
end;

theorem Th17:
   for G1,G2 being Go-board st Values G1 c= Values G2 &
       1 <= i1 & i1 <= len G1 & 1 < j1 & j1 <= width G1 &
       1 <= i2 & i2 <= len G2 & 1 < j2 & j2 <= width G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds G1*(i1,j1-'1)`2 <= G2*(i2,j2-'1)`2
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  1 <= i1 & i1 <= len G1 and
A3:  1 < j1 & j1 <= width G1 and
A4:  1 <= i2 & i2 <= len G2 and
A5:  1 < j2 & j2 <= width G2 and
A6:  G1*(i1,j1) = G2*(i2,j2);
 set p = G1*(i1,j1-'1);
 assume
A7:  G2*(i2,j2-'1)`2 < p`2;
A8:  1 <= j1-'1 by A3,JORDAN3:12;
then A9:  j1-'1 < j1 by JORDAN3:14;
 then j1-'1 < width G1 by A3,AXIOMS:22;
 then [i1,j1-'1] in Indices G1 by A2,A8,GOBOARD7:10;
 then p in {G1*(i,j): [i,j] in Indices G1};
 then p in Values G1 by Th7;
 then p in Values G2 by A1;
 then p in {G2*(i,j): [i,j] in Indices G2} by Th7;
 then consider i,j such that
A10:  p = G2*(i,j) and
A11:  [i,j] in Indices G2;
A12: 1 <= i & i <= len G2 & 1 <= j & j <= width G2 by A11,GOBOARD5:1;
then A13:  G2*(i,j)`2 = G2*(1,j)`2 by GOBOARD5:2
               .= G2*(i2,j)`2 by A4,A12,GOBOARD5:2;
then A14:  G2*(i2,j)`2 < G2*(i2,j2)`2 by A2,A3,A6,A8,A9,A10,GOBOARD5:5;
A15: now assume j2 <= j;
     then j = j2 or j2 < j by REAL_1:def 5;
     hence contradiction by A4,A5,A12,A14,GOBOARD5:5;
    end;
   1 <= j2-'1 by A5,JORDAN3:12;
 then j2-'1 < j2 by JORDAN3:14;
then A16:  j2-'1 < width G2 by A5,AXIOMS:22;
     now assume j <= j2-'1;
     then j2-'1 = j or j < j2-'1 by REAL_1:def 5;
     hence contradiction by A4,A7,A10,A12,A13,A16,GOBOARD5:5;
   end;
 hence contradiction by A15,JORDAN3:12;
end;

Lm1: for M being Matrix of D st
       1 <= i & i <= len M & 1 <= j & j <= width M holds
      M*(i,j) in Values M
proof
  let M be Matrix of D;
A1:  Values M = { M*(i1,j1): [i1,j1] in Indices M } by Th7;
  assume 1 <= i & i <= len M & 1 <= j & j <= width M;
  then [i,j] in Indices M by GOBOARD7:10;
  hence thesis by A1;
end;

theorem Th18:
   for G1,G2 being Go-board st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & [i2,j2] in Indices G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds cell(G2,i2,j2) c= cell(G1,i1,j1)
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  [i2,j2] in Indices G2 and
A4:  G1*(i1,j1) = G2*(i2,j2);
 let p be set such that
A5:  p in cell(G2,i2,j2);
A6:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
A7:  1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 by A3,GOBOARD5:1;
A8:  G1*(i1,j1)`1 = G1*(i1,1)`1 & G1*(i1,j1)`2 = G1*(1,j1)`2
       by A6,GOBOARD5:2,3;
A9:  G2*(i2,j2)`1 = G2*(i2,1)`1 & G2*(i2,j2)`2 = G2*(1,j2)`2
       by A7,GOBOARD5:2,3;
  per cases by A7,REAL_1:def 5;
  suppose
A10:  i2 = len G2 & j2 = width G2;
then A11:  i1 = len G1 & j1 = width G1 by A1,A2,A4,A7,Th11,Th13;
     p in { |[r,s]| : G2*(i2,j2)`1 <= r & G2*(i2,j2)`2 <= s }
    by A5,A9,A10,GOBRD11:28;
   hence p in cell(G1,i1,j1) by A4,A8,A11,GOBRD11:28;
  suppose
A12:  i2 = len G2 & j2 < width G2;
then A13:  i1 = len G1 by A1,A2,A4,A7,Th11;
     p in
 { |[r,s]| : G2*(i2,j2)`1 <= r & G2*(i2,j2)`2 <= s & s <= G2*(1,j2+1)`2 }
    by A5,A7,A9,A12,GOBRD11:29;
   then consider r',s' such that
A14:  p = |[r',s']| and
A15:  G2*(i2,j2)`1 <= r' & G2*(i2,j2)`2 <= s' and
A16:  s' <= G2*(1,j2+1)`2;
      now per cases by A6,REAL_1:def 5;
     suppose
A17:    j1 = width G1;
        p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s} by A4,A14,A15;
      hence p in cell(G1,i1,j1) by A8,A13,A17,GOBRD11:28;
     suppose
A18:     j1 < width G1;
then A19:    1 <= j1+1 & j1+1 <= width G1 & 1 <= j2+1 & j2+1 <= width G2
       by A12,NAT_1:37,38;
      then A20: G1*(i1,j1+1) in Values G1 by A6,Lm1;
        G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2
       by A6,A7,A19,GOBOARD5:2;
      then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A6,A7,A12,A18,A20,Th16;
      then s' <= G1*(1,j1+1)`2 by A16,AXIOMS:22;
      then p in {|[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s & s <=
 G1*(1,j1+1)`2}
       by A4,A14,A15;
      hence p in cell(G1,i1,j1) by A6,A8,A13,A18,GOBRD11:29;
    end;
   hence p in cell(G1,i1,j1);
  suppose
A21:  i2 < len G2 & j2 = width G2;
then A22:  j1 = width G1 by A1,A2,A4,A7,Th13;
      p in {|[r,s]|: G2*(i2,j2)`1 <= r & r <= G2*(i2+1,1)`1 &
      G2*(i2,j2)`2 <= s} by A5,A7,A9,A21,GOBRD11:31;
   then consider r',s' such that
A23:  p = |[r',s']| and
A24:  G2*(i2,j2)`1 <= r' and
A25:  r' <= G2*(i2+1,1)`1 and
A26:  G2*(i2,j2)`2 <= s';
      now per cases by A6,REAL_1:def 5;
     suppose
A27:    i1 = len G1;
        p in
 { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s} by A4,A23,A24,A26;
      hence p in cell(G1,i1,j1) by A8,A22,A27,GOBRD11:28;
     suppose
A28:    i1 < len G1;
      then 1 <= i1+1 & i1+1 <= len G1 & 1 <= i2+1 & i2+1 <=
 len G2 by A21,NAT_1:37,38;
      then G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 & G1*(i1+1,j1)`1 = G1*(i1+1,1)`1
       by A6,A7,GOBOARD5:3;
      then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1
       by A1,A4,A6,A7,A21,A28,Th14;
      then r' <= G1*(i1+1,1)`1 by A25,AXIOMS:22;
      then p in
 {|[r,s]|: G1*(i1,j1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*(i1,j1)`2 <= s}
       by A4,A23,A24,A26;
      hence p in cell(G1,i1,j1) by A6,A8,A22,A28,GOBRD11:31;
    end;
   hence p in cell(G1,i1,j1);
  suppose
A29:  i2 < len G2 & j2 < width G2;
 then 1 <= i2+1 & i2+1 <= len G2 & 1 <= j2+1 & j2+1 <= width G2 by NAT_1:37,38
;
 then G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 & G2*(i2,j2+1)`2 = G2*(1,j2+1)`2
       by A7,GOBOARD5:2,3;
   then p in { |[r,s]| : G2*(i2,j2)`1 <= r & r <= G2*(i2+1,j2)`1 &
                        G2*(i2,j2)`2 <= s & s <= G2*(i2,j2+1)`2 }
    by A5,A7,A9,A29,GOBRD11:32;
   then consider r',s' such that
A30:  p = |[r',s']| and
A31:  G2*(i2,j2)`1 <= r' and
A32:  r' <= G2*(i2+1,j2)`1 and
A33:  G2*(i2,j2)`2 <= s' and
A34:  s' <= G2*(i2,j2+1)`2;
     now per cases by A6,REAL_1:def 5;
   suppose
A35:  i1 = len G1 & j1 = width G1;
      p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s }
      by A4,A30,A31,A33;
    hence p in cell(G1,i1,j1) by A8,A35,GOBRD11:28;
   suppose
A36:  i1 = len G1 & j1 < width G1;
then A37:  1 <= j1+1 & j1+1 <= width G1 by NAT_1:37,38;
    then A38: G1*(i1,j1+1) in Values G1 by A6,Lm1;
      G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A6,A37,GOBOARD5:2;
    then G2*(i2,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A6,A7,A29,A36,A38,Th16;
    then s' <= G1*(1,j1+1)`2 by A34,AXIOMS:22;
    then p in {|[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s & s <= G1*
(1,j1+1)`2}
       by A4,A30,A31,A33;
    hence p in cell(G1,i1,j1) by A6,A8,A36,GOBRD11:29;
   suppose
A39:  i1 < len G1 & j1 = width G1;
    then 1 <= i1+1 & i1+1 <= len G1 by NAT_1:37,38;
    then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A6,GOBOARD5:3;
    then G2*(i2+1,j2)`1 <= G1*(i1+1,1)`1 by A1,A4,A6,A7,A29,A39,Th14;
    then r' <= G1*(i1+1,1)`1 by A32,AXIOMS:22;
    then p in {|[r,s]|: G1*(i1,j1)`1 <= r & r <= G1*(i1+1,1)`1 &
     G1*(i1,j1)`2 <= s} by A4,A30,A31,A33;
    hence p in cell(G1,i1,j1) by A6,A8,A39,GOBRD11:31;
   suppose
A40:  i1 < len G1 & j1 < width G1;
then A41:  1 <= j1+1 & j1+1 <= width G1 & 1 <= i1+1 & i1+1 <= len G1 by NAT_1:
37,38;
    then A42: G1*(i1,j1+1) in Values G1 by A6,Lm1;
      G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 & G1*(i1+1,j1)`1 = G1*(i1+1,1)`1
     by A6,A41,GOBOARD5:2,3;
    then G2*(i2,j2+1)`2 <= G1*(1,j1+1)`2 & G2*(i2+1,j2)`1 <= G1*(i1+1,1)`1
     by A1,A4,A6,A7,A29,A40,A42,Th14,Th16;
    then s' <= G1*(1,j1+1)`2 & r' <= G1*(i1+1,1)`1 by A32,A34,AXIOMS:22;
    then p in { |[r,s]| : G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 &
                         G1*(1,j1)`2 <= s & s <= G1*(1,j1+1)`2 }
     by A4,A8,A30,A31,A33;
    hence p in cell(G1,i1,j1) by A6,A40,GOBRD11:32;
   end;
   hence p in cell(G1,i1,j1);
end;

theorem Th19:
   for G1,G2 being Go-board st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & [i2,j2] in Indices G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds cell(G2,i2-'1,j2) c= cell(G1,i1-'1,j1)
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  [i2,j2] in Indices G2 and
A4:  G1*(i1,j1) = G2*(i2,j2);
 let p be set such that
A5:  p in cell(G2,i2-'1,j2);
A6:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
A7:  1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 by A3,GOBOARD5:1;
then A8:  G2*(i2,j2)`1 = G2*(i2,1)`1 & G2*(i2,j2)`2 = G2*(1,j2)`2
       by GOBOARD5:2,3;
  per cases by A6,A7,REAL_1:def 5;
  suppose
A9:  i1 = 1 & i2 = 1;
then A10:  i1-'1 = 0 & i2-'1 = 0 by GOBOARD9:1;
     now per cases by A7,REAL_1:def 5;
   suppose
A11:  j2 = width G2;
    then p in { |[r,s]| : r <= G2*(1,1)`1 & G2*(1,width G2)`2 <= s }
     by A5,A10,GOBRD11:25;
    then consider r',s' such that
A12:  p = |[r',s']| and
A13:  r' <= G2*(1,1)`1 and
A14:  G2*(1,width G2)`2 <= s';
A15:  j1 = width G1 by A1,A2,A4,A7,A11,Th13;
      G2*(1,1)`1 = G2*(i1,j2)`1 by A7,A9,GOBOARD5:3;
    then r' <= G1*(1,1)`1 by A4,A6,A9,A13,GOBOARD5:3;
    then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
     by A4,A9,A11,A12,A14,A15;
    hence thesis by A10,A15,GOBRD11:25;
   suppose
A16:  j2 < width G2;
    then p in
 {|[r,s]|: r <= G2*(1,1)`1 & G2*(1,j2)`2 <= s & s <= G2*(1,j2+1)`2}
     by A5,A7,A10,GOBRD11:26;
    then consider r',s' such that
A17:  p = |[r',s']| and
A18:  r' <= G2*(1,1)`1 and
A19:  G2*(1,j2)`2 <= s' and
A20:  s' <= G2*(1,j2+1)`2;
      G2*(1,1)`1 = G2*(i1,j2)`1 by A7,A9,GOBOARD5:3;
then A21:    r' <= G1*(1,1)`1 by A4,A6,A9,A18,GOBOARD5:3;
      now per cases by A6,REAL_1:def 5;
     suppose
A22:     j1 = width G1;
      then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
       by A4,A9,A17,A19,A21;
      hence thesis by A10,A22,GOBRD11:25;
     suppose
A23:  j1 < width G1;
      then 1 <= j1 + 1 & j1 + 1 <= width G1 by NAT_1:29,38;
      then G1*(i1,j1+1) in Values G1 by A6,Lm1;
      then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A6,A7,A9,A16,A23,Th16;
      then s' <= G1*(1,j1+1)`2 by A20,AXIOMS:22;
      then p in {|[r,s]|: r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s & s <=
 G1*(1,j1+1)`2}
       by A4,A9,A17,A19,A21;
      hence thesis by A6,A10,A23,GOBRD11:26;
    end;
    hence thesis;
   end;
   hence thesis;
  suppose that
A24:  i1 = 1 and
A25:  1 < i2;
A26:  i1-'1 = 0 by A24,GOBOARD9:1;
A27: 1 <= i2-'1 by A25,JORDAN3:12;
    then i2-'1 < i2 by JORDAN3:14;
then A28:  i2-'1 < len G2 by A7,AXIOMS:22;
A29:  i2-'1+1 = i2 by A25,AMI_5:4;
     now per cases by A7,REAL_1:def 5;
   suppose
A30:  j2 = width G2;
    then p in { |[r,s]|: G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 &
    G2*(1,j2)`2 <= s} by A5,A27,A28,A29,GOBRD11:31;
    then consider r',s' such that
A31:  p = |[r',s']| and G2*(i2-'1,1)`1 <= r' and
A32:  r' <= G2*(i2,1)`1 and
A33:  G2*(1,j2)`2 <= s';
A34:  j1 = width G1 by A1,A2,A4,A7,A30,Th13;
A35:    r' <= G1*(1,1)`1 by A4,A6,A8,A24,A32,GOBOARD5:3;
      G1*(1,j1)`2 <= s' by A4,A6,A8,A33,GOBOARD5:2;
    then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s } by A31,A35;
    hence thesis by A26,A34,GOBRD11:25;
   suppose
A36:  j2 < width G2;
    then p in { |[r,s]| : G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 &
                    G2*(1,j2)`2 <= s & s <= G2*(1,j2+1)`2 }
      by A5,A7,A27,A28,A29,GOBRD11:32;
    then consider r',s' such that
A37:  p = |[r',s']| and G2*(i2-'1,1)`1 <= r' and
A38:  r' <= G2*(i2,1)`1 and
A39:  G2*(1,j2)`2 <= s' and
A40:  s' <= G2*(1,j2+1)`2;
A41:   r' <= G1*(1,1)`1 by A4,A6,A8,A24,A38,GOBOARD5:3;
A42:   G1*(1,j1)`2 <= s' by A4,A6,A8,A39,GOBOARD5:2;
      now per cases by A6,REAL_1:def 5;
     suppose
A43:     j1 = width G1;
      then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
       by A37,A41,A42;
      hence thesis by A26,A43,GOBRD11:25;
     suppose
A44:    j1 < width G1;
then A45:    1 <= j1+1 & j1+1 <= width G1 & 1 <= j2+1 & j2+1 <= width G2
       by A36,NAT_1:37,38;
      then A46: G1*(i1,j1+1) in Values G1 by A6,Lm1;
        G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 & G2*(i2,j2+1)`2 = G2*(1,j2+1)`2
        by A6,A7,A45,GOBOARD5:2;
      then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A6,A7,A36,A44,A46,Th16;
      then s' <= G1*(1,j1+1)`2 by A40,AXIOMS:22;
      then p in {|[r,s]|: r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s &
      s <= G1*(1,j1+1)`2} by A37,A41,A42;
      hence thesis by A6,A26,A44,GOBRD11:26;
    end;
    hence thesis;
   end;
   hence thesis;
  suppose 1 < i1 & i2 = 1;
    hence thesis by A1,A2,A4,A7,Th10;
  suppose
A47:  1 < i1 & 1 < i2;
then A48:  1 <= i1-'1 & 1 <= i2-'1 by JORDAN3:12;
 then i1-'1 < i1 & i2-'1 < i2 by JORDAN3:14;
then A49:  i1-'1 < len G1 & i2-'1 < len G2 by A6,A7,AXIOMS:22;
A50:  i1-'1+1 = i1 & i2-'1+1 = i2 by A48,JORDAN3:6;
      A51: G1*(i1-'1,j1) in Values G1 by A6,A48,A49,Lm1;
    G1*(i1-'1,1)`1 = G1*(i1-'1,j1)`1 & G2*(i2-'1,1)`1 = G2*(i2-'1,j2)`1
      by A6,A7,A48,A49,GOBOARD5:3;
then A52:  G1*(i1-'1,1)`1 <= G2*(i2-'1,1)`1 by A1,A4,A6,A7,A47,A51,Th15;
     now per cases by A7,REAL_1:def 5;
   suppose
A53:  j2 = width G2;
    then p in { |[r,s]|: G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 &
    G2*(1,j2)`2 <= s} by A5,A48,A49,A50,GOBRD11:31;
    then consider r',s' such that
A54:  p = |[r',s']| and
A55:  G2*(i2-'1,1)`1 <= r' and
A56:  r' <= G2*(i2,1)`1 and
A57:  G2*(1,j2)`2 <= s';
A58:  j1 = width G1 by A1,A2,A4,A7,A53,Th13;
A59:  G1*(i1-'1,1)`1 <= r' by A52,A55,AXIOMS:22;
A60:  r' <= G1*(i1,1)`1 by A4,A6,A8,A56,GOBOARD5:3;
      G1*(1,j1)`2 <= s' by A4,A6,A8,A57,GOBOARD5:2;
    then p in { |[r,s]|: G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 &
    G1*(1,j1)`2 <= s} by A54,A59,A60;
    hence thesis by A48,A49,A50,A58,GOBRD11:31;
   suppose
A61:  j2 < width G2;
    then p in { |[r,s]| : G2*(i2-'1,1)`1 <= r & r <= G2*(i2,1)`1 &
                    G2*(1,j2)`2 <= s & s <= G2*(1,j2+1)`2 }
      by A5,A7,A48,A49,A50,GOBRD11:32;
    then consider r',s' such that
A62:  p = |[r',s']| and
A63:  G2*(i2-'1,1)`1 <= r' and
A64:  r' <= G2*(i2,1)`1 and
A65:  G2*(1,j2)`2 <= s' and
A66:  s' <= G2*(1,j2+1)`2;
A67:  G1*(i1-'1,1)`1 <= r' by A52,A63,AXIOMS:22;
A68:  r' <= G1*(i1,1)`1 by A4,A6,A8,A64,GOBOARD5:3;
A69:  G1*(1,j1)`2 <= s' by A4,A6,A8,A65,GOBOARD5:2;
      now per cases by A6,REAL_1:def 5;
     suppose
A70:    j1 = width G1;
        p in { |[r,s]|: G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 &
      G1*(1,j1)`2 <= s } by A62,A67,A68,A69;
      hence thesis by A48,A49,A50,A70,GOBRD11:31;
     suppose
A71:    j1 < width G1;
      then A72: 1 <= j1+1 & j1+1 <= width G1 & 1 <= j2+1 & j2+1 <= width G2
       by A61,NAT_1:37,38;
      then A73: G1*(i1,j1+1) in Values G1 by A6,Lm1;
        G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 & G2*(i2,j2+1)`2 = G2*(1,j2+1)`2
        by A6,A7,A72,GOBOARD5:2;
      then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A6,A7,A61,A71,A73,Th16;
      then s' <= G1*(1,j1+1)`2 by A66,AXIOMS:22;
      then p in { |[r,s]| : G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 &
                           G1*(1,j1)`2 <= s & s <= G1*(1,j1+1)`2 }
         by A62,A67,A68,A69;
      hence thesis by A6,A48,A49,A50,A71,GOBRD11:32;
    end;
    hence thesis;
   end;
   hence thesis;
end;

theorem Th20:
   for G1,G2 being Go-board
    st Values G1 c= Values G2 &
       [i1,j1] in Indices G1 & [i2,j2] in Indices G2 &
       G1*(i1,j1) = G2*(i2,j2)
   holds cell(G2,i2,j2-'1) c= cell(G1,i1,j1-'1)
proof let G1,G2 be Go-board such that
A1:  Values G1 c= Values G2 and
A2:  [i1,j1] in Indices G1 and
A3:  [i2,j2] in Indices G2 and
A4:  G1*(i1,j1) = G2*(i2,j2);
 let p be set such that
A5:  p in cell(G2,i2,j2-'1);
A6:  1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 by A2,GOBOARD5:1;
A7:  1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 by A3,GOBOARD5:1;
A8:  G1*(i1,j1)`1 = G1*(i1,1)`1 & G1*(i1,j1)`2 = G1*(1,j1)`2
       by A6,GOBOARD5:2,3;
A9:  G2*(i2,j2)`1 = G2*(i2,1)`1 & G2*(i2,j2)`2 = G2*(1,j2)`2
       by A7,GOBOARD5:2,3;
  per cases by A6,A7,REAL_1:def 5;
  suppose
A10:  j1 = 1 & j2 = 1;
then A11:  j1-'1 = 0 & j2-'1 = 0 by GOBOARD9:1;
     now per cases by A7,REAL_1:def 5;
   suppose
A12:  i2 = len G2;
    then p in { |[r,s]| : G2*(len G2,1)`1 <= r & s <= G2*(1,1)`2 }
     by A5,A11,GOBRD11:27;
    then consider r',s' such that
A13:  p = |[r',s']| and
A14:  G2*(len G2,1)`1 <= r' and
A15:  s' <= G2*(1,1)`2;
A16:  i1 = len G1 by A1,A2,A4,A7,A12,Th11;
      G2*(1,1)`2 = G2*(i2,j2)`2 by A7,A10,GOBOARD5:2;
    then s' <= G1*(1,1)`2 by A4,A6,A10,A15,GOBOARD5:2;
    then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 }
     by A4,A10,A12,A13,A14,A16;
    hence thesis by A11,A16,GOBRD11:27;
   suppose
A17:  i2 < len G2;
    then p in {|[r,s]|: G2*(i2,1)`1 <= r & r <= G2*(i2+1,1)`1 & s <=
 G2*(1,1)`2 }
     by A5,A7,A11,GOBRD11:30;
    then consider r',s' such that
A18:  p = |[r',s']| and
A19:  G2*(i2,1)`1 <= r' and
A20:  r' <= G2*(i2+1,1)`1 and
A21:  s' <= G2*(1,1)`2;
      G2*(1,1)`2 = G2*(i2,j1)`2 by A7,A10,GOBOARD5:2;
then A22:    s' <= G1*(1,1)`2 by A4,A6,A10,A21,GOBOARD5:2;
      now per cases by A6,REAL_1:def 5;
     suppose
A23:     i1 = len G1;
      then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 }
       by A4,A10,A18,A19,A22;
      hence thesis by A11,A23,GOBRD11:27;
     suppose
A24:    i1 < len G1;
      then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A6,A7,A10,A17,Th14;
      then r' <= G1*(i1+1,1)`1 by A20,AXIOMS:22;
      then p in {|[r,s]|: G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & s <=
 G1*(1,1)`2}
       by A4,A10,A18,A19,A22;
      hence thesis by A6,A11,A24,GOBRD11:30;
    end;
    hence thesis;
   end;
   hence thesis;
  suppose that
A25:  j1 = 1 and
A26:  1 < j2;
A27:  j1-'1 = 0 by A25,GOBOARD9:1;
A28: 1 <= j2-'1 by A26,JORDAN3:12;
    then j2-'1 < j2 by JORDAN3:14;
then A29:  j2-'1 < width G2 by A7,AXIOMS:22;
A30:  j2-'1+1 = j2 by A26,AMI_5:4;
     now per cases by A7,REAL_1:def 5;
   suppose
A31:  i2 = len G2;
then A32:  i1 = len G1 by A1,A2,A4,A7,Th11;
      p in
 { |[r,s]| : G2*(i2,1)`1 <= r & G2*(1,j2-'1)`2 <= s & s <= G2*(1,j2)`2 }
     by A5,A28,A29,A30,A31,GOBRD11:29;
     then ex r',s' st p = |[r',s']| & G2*(i2,1)`1 <= r' & G2*(1,j2-'1)`2 <= s'
&
      s' <= G2*(1,j2)`2;
     then p in
 { |[r,s]| : G1*(i1,1)`1 <= r & s <= G1*(1,1)`2 } by A4,A8,A9,A25;
    hence thesis by A27,A32,GOBRD11:27;
   suppose
A33:  i2 < len G2;
    then p in { |[r,s]| : G2*(i2,1)`1 <= r & r <= G2*(i2+1,1)`1 &
                    G2*(1,j2-'1)`2 <= s & s <= G2*(1,j2)`2 }
      by A5,A7,A28,A29,A30,GOBRD11:32;
    then consider r',s' such that
A34:  p = |[r',s']| and
A35:  G2*(i2,1)`1 <= r' and
A36:  r' <= G2*(i2+1,1)`1 and G2*(1,j2-'1)`2 <= s' and
A37:  s' <= G2*(1,j2)`2;
A38:   s' <= G1*(1,1)`2 by A4,A7,A8,A25,A37,GOBOARD5:2;
A39:   G1*(i1,1)`1 <= r' by A4,A7,A8,A35,GOBOARD5:3;
      now per cases by A6,REAL_1:def 5;
     suppose
A40:    i1 = len G1;
      then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 }
       by A34,A38,A39;
      hence thesis by A27,A40,GOBRD11:27;
     suppose
A41:    i1 < len G1;
      then 1 <= i1+1 & i1+1 <= len G1 & 1 <= i2+1 & i2+1 <= len G2
       by A33,NAT_1:37,38;
      then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 & G2*(i2+1,j2)`1 = G2*(i2+1,1)`1
        by A6,A7,GOBOARD5:3;
      then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A6,A7,A33,A41,Th14;
      then r' <= G1*(i1+1,1)`1 by A36,AXIOMS:22;
      then p in {|[r,s]|: G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & s <=
 G1*(1,1)`2}
       by A34,A38,A39;
      hence thesis by A6,A27,A41,GOBRD11:30;
    end;
    hence thesis;
   end;
   hence thesis;
  suppose 1 < j1 & j2 = 1;
    hence thesis by A1,A2,A4,A7,Th12;
  suppose
A42:  1 < j1 & 1 < j2;
then A43:  1 <= j1-'1 & 1 <= j2-'1 by JORDAN3:12;
   then j1-'1 < j1 & j2-'1 < j2 by JORDAN3:14;
then A44:  j1-'1 < width G1 & j2-'1 < width G2 by A6,A7,AXIOMS:22;
A45:  j1-'1+1 = j1 & j2-'1+1 = j2 by A43,JORDAN3:6;
    G1*(1,j1-'1)`2 = G1*(i1,j1-'1)`2 & G2*(1,j2-'1)`2 = G2*(i2,j2-'1)`2
      by A6,A7,A43,A44,GOBOARD5:2;
then A46:  G1*(1,j1-'1)`2 <= G2*(1,j2-'1)`2 by A1,A4,A6,A7,A42,Th17;
     now per cases by A7,REAL_1:def 5;
   suppose
A47:  i2 = len G2;
    then p in { |[r,s]| : G2*(i2,1)`1 <= r & G2*(1,j2-'1)`2 <= s & s <= G2*
(1,j2)`2}
     by A5,A43,A44,A45,GOBRD11:29;
    then consider r',s' such that
A48:  p = |[r',s']| and
A49:  G2*(i2,1)`1 <= r' and
A50:  G2*(1,j2-'1)`2 <= s' and
A51:  s' <= G2*(1,j2)`2;
A52:  i1 = len G1 by A1,A2,A4,A7,A47,Th11;
A53:  G1*(1,j1-'1)`2 <= s' by A46,A50,AXIOMS:22;
A54:  s' <= G1*(1,j1)`2 by A4,A6,A9,A51,GOBOARD5:2;
      G1*(i1,1)`1 <= r' by A4,A6,A9,A49,GOBOARD5:3;
    then p in {|[r,s]|: G1*(i1,1)`1 <= r & G1*(1,j1-'1)`2 <= s & s <=
 G1*(1,j1)`2}
      by A48,A53,A54;
    hence thesis by A43,A44,A45,A52,GOBRD11:29;
   suppose
A55:  i2 < len G2;
    then p in { |[r,s]| : G2*(i2,1)`1 <= r & r <= G2*(i2+1,1)`1 &
                    G2*(1,j2-'1)`2 <= s & s <= G2*(1,j2)`2 }
      by A5,A7,A43,A44,A45,GOBRD11:32;
    then consider r',s' such that
A56:  p = |[r',s']| and
A57:  G2*(i2,1)`1 <= r' and
A58:  r' <= G2*(i2+1,1)`1 and
A59:  G2*(1,j2-'1)`2 <= s' and
A60:  s' <= G2*(1,j2)`2;
A61:  G1*(1,j1-'1)`2 <= s' by A46,A59,AXIOMS:22;
A62:  s' <= G1*(1,j1)`2 by A4,A6,A9,A60,GOBOARD5:2;
A63:  G1*(i1,1)`1 <= r' by A4,A6,A9,A57,GOBOARD5:3;
      now per cases by A6,REAL_1:def 5;
     suppose
A64:    i1 = len G1;
        p in {|[r,s]|: G1*(i1,1)`1 <= r & G1*(1,j1-'1)`2 <= s & s <= G1*
(1,j1)`2}
       by A56,A61,A62,A63;
      hence thesis by A43,A44,A45,A64,GOBRD11:29;
     suppose
A65:    i1 < len G1;
      then 1 <= i1+1 & i1+1 <= len G1 & 1 <= i2+1 & i2+1 <= len G2
       by A55,NAT_1:37,38;
      then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 & G2*(i2+1,j2)`1 = G2*(i2+1,1)`1
        by A6,A7,GOBOARD5:3;
      then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A6,A7,A55,A65,Th14;
      then r' <= G1*(i1+1,1)`1 by A58,AXIOMS:22;
      then p in { |[r,s]| : G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 &
                           G1*(1,j1-'1)`2 <= s & s <= G1*(1,j1)`2 }
         by A56,A61,A62,A63;
      hence thesis by A6,A43,A44,A45,A65,GOBRD11:32;
    end;
    hence thesis;
   end;
   hence thesis;
end;

Lm2:
  for f being non empty FinSequence of TOP-REAL 2
     st 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f
    ex k st k in dom f & (f/.k)`1 = (GoB f)*(i,j)`1
 proof let f be non empty FinSequence of TOP-REAL 2;
  assume
A1:  1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f;
then A2: [i,j] in Indices GoB f by GOBOARD7:10;
A3:  GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 3;
   then len Incr X_axis f = len GoB f by GOBOARD2:def 1;
   then i in dom Incr X_axis f by A1,FINSEQ_3:27;
   then (Incr X_axis f).i in rng Incr X_axis f by FUNCT_1:def 5;
   then (Incr X_axis f).i in rng X_axis f by GOBOARD2:def 2;
   then consider k such that
A4:  k in dom X_axis f and
A5:  (X_axis f).k = (Incr X_axis f).i by FINSEQ_2:11;
  take k;
     len X_axis f = len f by GOBOARD1:def 3;
  hence k in dom f by A4,FINSEQ_3:31;
A6: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]|
     by A2,A3,GOBOARD2:def 1;
  thus (f/.k)`1 = Incr(X_axis f).i by A4,A5,GOBOARD1:def 3
               .= (GoB f)*(i,j)`1 by A6,EUCLID:56;
 end;

Lm3:
  for f being non empty FinSequence of TOP-REAL 2
     st 1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f
    ex k st k in dom f & (f/.k)`2 = (GoB f)*(i,j)`2
 proof let f be non empty FinSequence of TOP-REAL 2;
  assume
A1:   1 <= i & i <= len GoB f & 1 <= j & j <= width GoB f;
then A2: [i,j] in Indices GoB f by GOBOARD7:10;
A3:   GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 3;
   then len Incr Y_axis f = width GoB f by GOBOARD2:def 1;
   then j in dom Incr Y_axis f by A1,FINSEQ_3:27;
   then (Incr Y_axis f).j in rng Incr Y_axis f by FUNCT_1:def 5;
   then (Incr Y_axis f).j in rng Y_axis f by GOBOARD2:def 2;
   then consider k such that
A4:   k in dom Y_axis f and
A5:   (Y_axis f).k = (Incr Y_axis f).j by FINSEQ_2:11;
  take k;
     len Y_axis f = len f by GOBOARD1:def 4;
  hence k in dom f by A4,FINSEQ_3:31;
A6: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]|
     by A2,A3,GOBOARD2:def 1;
  thus (f/.k)`2 = Incr(Y_axis f).j by A4,A5,GOBOARD1:def 4
               .= (GoB f)*(i,j)`2 by A6,EUCLID:56;
 end;

theorem Th21:
  for f being standard special_circular_sequence
    st f is_sequence_on G
   holds Values GoB f c= Values G
proof let f be standard special_circular_sequence such that
A1: f is_sequence_on G;
  set F = GoB f;
  let p be set; assume
    p in Values F;
  then p in { F*(i,j): [i,j] in Indices F } by Th7;
  then consider i,j such that
A2:  p = F*(i,j) and
A3:  [i,j] in Indices F;
A4:  1 <= i & i <= len F & 1 <= j & j <= width F by A3,GOBOARD5:1;
  reconsider p as Point of TOP-REAL 2 by A2;
  consider k1 such that
A5:  k1 in dom f and
A6:  p`1 = (f/.k1)`1 by A2,A4,Lm2;
  consider k2 such that
A7:  k2 in dom f and
A8:  p`2 = (f/.k2)`2 by A2,A4,Lm3;
  consider i1,j1 such that
A9:  [i1,j1] in Indices G and
A10:  f/.k1 = G*(i1,j1) by A1,A5,GOBOARD1:def 11;
A11:  1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A9,GOBOARD5:1;
  consider i2,j2 such that
A12:  [i2,j2] in Indices G and
A13:  f/.k2 = G*(i2,j2) by A1,A7,GOBOARD1:def 11;
A14:  1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A12,GOBOARD5:1;
then A15:  G*(i1,j2)`1 = G*(i1,1)`1 by A11,GOBOARD5:3
                .= G*(i1,j1)`1 by A11,GOBOARD5:3;
A16:  G*(i1,j2)`2 = G*(1,j2)`2 by A11,A14,GOBOARD5:2
                .= G*(i2,j2)`2 by A14,GOBOARD5:2;
A17:  [i1,j2] in Indices G by A11,A14,GOBOARD7:10;
    p = |[p`1, p`2]| by EUCLID:57;
  then p = G*(i1,j2) by A6,A8,A10,A13,A15,A16,EUCLID:57;
  then p in { G*(k,l): [k,l] in Indices G } by A17;
  hence thesis by Th7;
end;

definition let f, G, k;
  assume that
A1:  1 <= k & k+1 <= len f and
A2:  f is_sequence_on G;
   consider i1,j1,i2,j2 being Nat such that
A3:  [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A4:  [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A5:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,JORDAN8:6;

 func right_cell(f,k,G) -> Subset of TOP-REAL 2 means
 :Def2:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & it = cell(G,i1,j1) or
    i1+1 = i2 & j1 = j2 & it = cell(G,i1,j1-'1) or
    i1 = i2+1 & j1 = j2 & it = cell(G,i2,j2) or
    i1 = i2 & j1 = j2+1 & it = cell(G,i1-'1,j2);
 existence
  proof
   per cases by A5;
   suppose
A6:  i1 = i2 & j1+1 = j2;
     take cell(G,i1,j1);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A6;
   suppose
A7:  i1+1 = i2 & j1 = j2;
     take cell(G,i1,j1-'1);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A7;
   suppose
A8:  i1 = i2+1 & j1 = j2;
     take cell(G,i2,j2);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A8;
   suppose
A9:  i1 = i2 & j1 = j2+1;
     take cell(G,i1-'1,j2);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A9;
  end;
 uniqueness
  proof let P1,P2 be Subset of TOP-REAL 2 such that
A10: for i1,j1,i2,j2 being Nat st
      [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
    i1 = i2 & j1+1 = j2 & P1 = cell(G,i1,j1) or
    i1+1 = i2 & j1 = j2 & P1 = cell(G,i1,j1-'1) or
    i1 = i2+1 & j1 = j2 & P1 = cell(G,i2,j2) or
    i1 = i2 & j1 = j2+1 & P1 = cell(G,i1-'1,j2) and
A11: for i1,j1,i2,j2 being Nat st
      [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
    i1 = i2 & j1+1 = j2 & P2 = cell(G,i1,j1) or
    i1+1 = i2 & j1 = j2 & P2 = cell(G,i1,j1-'1) or
    i1 = i2+1 & j1 = j2 & P2 = cell(G,i2,j2) or
    i1 = i2 & j1 = j2+1 & P2 = cell(G,i1-'1,j2);
   per cases by A5;
   suppose i1 = i2 & j1+1 = j2;
then A12: j1 < j2 by REAL_1:69;
A13: j2 <= j2+1 by NAT_1:29;
   hence P1 = cell(G,i1,j1) by A3,A4,A10,A12 .= P2 by A3,A4,A11,A12,A13;
   suppose i1+1 = i2 & j1 = j2;
then A14: i1 < i2 by REAL_1:69;
A15: i2 <= i2+1 by NAT_1:29;
   hence P1 = cell(G,i1,j1-'1) by A3,A4,A10,A14 .= P2 by A3,A4,A11,A14,A15;
   suppose i1 = i2+1 & j1 = j2;
then A16: i2 < i1 by REAL_1:69;
A17: i1 <= i1+1 by NAT_1:29;
   hence P1 = cell(G,i2,j2) by A3,A4,A10,A16 .= P2 by A3,A4,A11,A16,A17;
   suppose i1 = i2 & j1 = j2+1;
then A18: j2 < j1 by REAL_1:69;
A19: j1 <= j1+1 by NAT_1:29;
   hence P1 = cell(G,i1-'1,j2) by A3,A4,A10,A18 .= P2 by A3,A4,A11,A18,A19;
  end;

 func left_cell(f,k,G) -> Subset of TOP-REAL 2 means
 :Def3:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & it = cell(G,i1-'1,j1) or
    i1+1 = i2 & j1 = j2 & it = cell(G,i1,j1) or
    i1 = i2+1 & j1 = j2 & it = cell(G,i2,j2-'1) or
    i1 = i2 & j1 = j2+1 & it = cell(G,i1,j2);
  existence
   proof
    per cases by A5;
    suppose
 A20:  i1 = i2 & j1+1 = j2;
     take cell(G,i1-'1,j1);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A20;
    suppose
 A21:  i1+1 = i2 & j1 = j2;
     take cell(G,i1,j1);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A21;
    suppose
 A22:  i1 = i2+1 & j1 = j2;
     take cell(G,i2,j2-'1);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A22;
    suppose
 A23:  i1 = i2 & j1 = j2+1;
     take cell(G,i1,j2);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A23;
   end;
  uniqueness
   proof let P1,P2 be Subset of TOP-REAL 2 such that
 A24: for i1,j1,i2,j2 being Nat st
       [i1,j1] in Indices G & [i2,j2] in Indices G &
       f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
     i1 = i2 & j1+1 = j2 & P1 = cell(G,i1-'1,j1) or
     i1+1 = i2 & j1 = j2 & P1 = cell(G,i1,j1) or
     i1 = i2+1 & j1 = j2 & P1 = cell(G,i2,j2-'1) or
     i1 = i2 & j1 = j2+1 & P1 = cell(G,i1,j2) and
 A25: for i1,j1,i2,j2 being Nat st
       [i1,j1] in Indices G & [i2,j2] in Indices G &
       f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
     i1 = i2 & j1+1 = j2 & P2 = cell(G,i1-'1,j1) or
     i1+1 = i2 & j1 = j2 & P2 = cell(G,i1,j1) or
     i1 = i2+1 & j1 = j2 & P2 = cell(G,i2,j2-'1) or
     i1 = i2 & j1 = j2+1 & P2 = cell(G,i1,j2);
    per cases by A5;
    suppose i1 = i2 & j1+1 = j2;
then A26:  j1 < j2 by REAL_1:69;
A27:  j2 <= j2+1 by NAT_1:29;
    hence P1 = cell(G,i1-'1,j1) by A3,A4,A24,A26 .= P2 by A3,A4,A25,A26,A27;
    suppose i1+1 = i2 & j1 = j2;
then A28:  i1 < i2 by REAL_1:69;
A29:  i2 <= i2+1 by NAT_1:29;
    hence P1 = cell(G,i1,j1) by A3,A4,A24,A28 .= P2 by A3,A4,A25,A28,A29;
    suppose i1 = i2+1 & j1 = j2;
then A30:  i2 < i1 by REAL_1:69;
A31:  i1 <= i1+1 by NAT_1:29;
    hence P1 = cell(G,i2,j2-'1) by A3,A4,A24,A30 .= P2 by A3,A4,A25,A30,A31;
    suppose i1 = i2 & j1 = j2+1;
then A32:  j2 < j1 by REAL_1:69;
A33:  j1 <= j1+1 by NAT_1:29;
    hence P1 = cell(G,i1,j2) by A3,A4,A24,A32 .= P2 by A3,A4,A25,A32,A33;
   end;
end;

theorem Th22:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i,j+1] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1)
  implies left_cell(f,k,G) = cell(G,i-'1,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i,j+1] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i,j+1);
A6: j < j+1 by REAL_1:69;
    j+1 <= j+1+1 by NAT_1:29;
  hence left_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,A4,A5,A6,Def3;
end;

theorem Th23:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i,j+1] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1)
  implies right_cell(f,k,G) = cell(G,i,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i,j+1] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i,j+1);
A6: j < j+1 by REAL_1:69;
    j+1 <= j+1+1 by NAT_1:29;
 hence right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,A5,A6,Def2;
end;

theorem Th24:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j)
  implies left_cell(f,k,G) = cell(G,i,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i+1,j);
A6: i < i+1 by REAL_1:69;
   i+1 <= i+1+1 by NAT_1:29;
 hence left_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,A5,A6,Def3;
end;

theorem Th25:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j)
  implies right_cell(f,k,G) = cell(G,i,j-'1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i+1,j);
A6: i < i+1 by REAL_1:69;
     i+1 <= i+1+1 by NAT_1:29;
hence right_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,A4,A5,A6,Def2;
end;

theorem Th26:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j)
  implies left_cell(f,k,G) = cell(G,i,j-'1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i+1,j) and
A5: f/.(k+1) = G*(i,j);
A6: i < i+1 by REAL_1:69;
   i+1 <= i+1+1 by NAT_1:29;
 hence left_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,A4,A5,A6,Def3;
end;

theorem Th27:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j)
  implies right_cell(f,k,G) = cell(G,i,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i+1,j) and
A5: f/.(k+1) = G*(i,j);
A6: i < i+1 by REAL_1:69;
     i+1 <= i+1+1 by NAT_1:29;
   hence right_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,A5,A6,Def2;
end;

theorem Th28:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j+1] in Indices G & [i,j] in Indices G &
 f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j)
  implies left_cell(f,k,G) = cell(G,i,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j+1] in Indices G & [i,j] in Indices G and
A4: f/.k = G*(i,j+1) and
A5: f/.(k+1) = G*(i,j);
A6: j < j+1 by REAL_1:69;
   j+1 <= j+1+1 by NAT_1:29;
 hence left_cell(f,k,G) = cell(G,i,j) by A1,A2,A3,A4,A5,A6,Def3;
end;

theorem Th29:
 1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j+1] in Indices G & [i,j] in Indices G &
 f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j)
   implies right_cell(f,k,G) = cell(G,i-'1,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j+1] in Indices G & [i,j] in Indices G and
A4: f/.k = G*(i,j+1) and
A5: f/.(k+1) = G*(i,j);
A6: j < j+1 by REAL_1:69;
     j+1 <= j+1+1 by NAT_1:29;
   hence right_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,A4,A5,A6,Def2;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G
  implies left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(f,k)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G;
      k <= k+1 by NAT_1:29;
    then k <= len f by A1,AXIOMS:22;
then A3:  k in dom f by A1,FINSEQ_3:27;
    then consider i1,j1 being Nat such that
A4:  [i1,j1] in Indices G & f/.k = G*(i1,j1) by A2,GOBOARD1:def 11;
      k+1 >= 1 by NAT_1:29;
then A5:  k+1 in dom f by A1,FINSEQ_3:27;
    then consider i2,j2 being Nat such that
A6:  [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) by A2,GOBOARD1:def 11;
A7:  abs(i1-i2)+abs(j1-j2) = 1 by A2,A3,A4,A5,A6,GOBOARD1:def 11;
A8: now per cases by A7,GOBOARD1:2;
     case that
A9:  abs(i1-i2) = 1 and
A10:  j1 = j2;
A11:   -(i1-i2) = i2-i1 by XCMPLX_1:143;
        i1-i2 >= 0 or i1-i2 < 0;
      then i1-i2 = 1 or -(i1-i2) = 1 by A9,ABSVALUE:def 1;
     hence i1 = i2+1 or i1+1 = i2 by A11,XCMPLX_1:27;
     thus j1 = j2 by A10;
     case that
A12:  i1 = i2 and
A13:  abs(j1-j2) = 1;
A14:   -(j1-j2) = j2-j1 by XCMPLX_1:143;
        j1-j2 >= 0 or j1-j2 < 0;
      then j1-j2 = 1 or -(j1-j2) = 1 by A13,ABSVALUE:def 1;
     hence j1 = j2+1 or j1+1 = j2 by A14,XCMPLX_1:27;
     thus i1 = i2 by A12;
    end;
A15: 0+1 <= j1 & j1 <= width G by A4,GOBOARD5:1;
A16: 1 <= j2 & j2 <= width G by A6,GOBOARD5:1;
A17: 0+1 <= i1 & i1 <= len G by A4,GOBOARD5:1;
A18: 1 <= i2 & i2 <= len G by A6,GOBOARD5:1;
     i1 > 0 by A17,NAT_1:38;
   then consider i such that
A19: i+1 = i1 by NAT_1:22;
A20: i < len G by A17,A19,NAT_1:38;
     j1 > 0 by A15,NAT_1:38;
   then consider j such that
A21: j+1 = j1 by NAT_1:22;
A22: j < width G by A15,A21,NAT_1:38;
A23:  i1-'1 = i & j1-'1=j by A19,A21,BINARITH:39;
   per cases by A8;
   suppose
A24:  i1 = i2 & j1+1 = j2;
then A25: j1 < width G by A16,NAT_1:38;
       left_cell(f,k,G) = cell(G,i,j1) & right_cell(f,k,G) = cell(G,i1,j1)
       by A1,A2,A4,A6,A23,A24,Th22,Th23;
    hence left_cell(f,k,G) /\ right_cell(f,k,G)
            = LSeg(G*(i1,j1),G*(i1,j1+1)) by A15,A19,A20,A25,GOBOARD5:26
           .= LSeg(f,k) by A1,A4,A6,A24,TOPREAL1:def 5;
   suppose
A26:  i1+1 = i2 & j1 = j2;
then A27: i1 < len G by A18,NAT_1:38;
       left_cell(f,k,G) = cell(G,i1,j1) & right_cell(f,k,G) = cell(G,i1,j)
        by A1,A2,A4,A6,A23,A26,Th24,Th25;
    hence left_cell(f,k,G) /\ right_cell(f,k,G)
            = LSeg(G*(i1,j1),G*(i1+1,j1)) by A17,A21,A22,A27,GOBOARD5:27
           .= LSeg(f,k) by A1,A4,A6,A26,TOPREAL1:def 5;
   suppose
A28:  i1 = i2+1 & j1 = j2;
then A29: i2 < len G by A17,NAT_1:38;
       left_cell(f,k,G) = cell(G,i2,j) & right_cell(f,k,G) = cell(G,i2,j1)
       by A1,A2,A4,A6,A23,A28,Th26,Th27;
    hence left_cell(f,k,G) /\ right_cell(f,k,G)
            = LSeg(G*(i2+1,j1),G*(i2,j1)) by A18,A21,A22,A29,GOBOARD5:27
           .= LSeg(f,k) by A1,A4,A6,A28,TOPREAL1:def 5;
   suppose
A30:  i1 = i2 & j1 = j2+1;
then A31: j2 < width G by A15,NAT_1:38;
       left_cell(f,k,G) = cell(G,i1,j2) & right_cell(f,k,G) = cell(G,i,j2)
       by A1,A2,A4,A6,A23,A30,Th28,Th29;
    hence left_cell(f,k,G) /\ right_cell(f,k,G)
            = LSeg(G*(i1,j2+1),G*(i1,j2)) by A16,A19,A20,A31,GOBOARD5:26
           .= LSeg(f,k) by A1,A4,A6,A30,TOPREAL1:def 5;
end;

theorem
     1 <= k & k+1 <= len f & f is_sequence_on G
    implies right_cell(f,k,G) is closed
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G;
   consider i1,j1,i2,j2 being Nat such that
A3:  [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A4:  [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A5:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,JORDAN8:6;
      i1 = i2 & j1+1 = j2 & right_cell(f,k,G) = cell(G,i1,j1) or
    i1+1 = i2 & j1 = j2 & right_cell(f,k,G) = cell(G,i1,j1-'1) or
    i1 = i2+1 & j1 = j2 & right_cell(f,k,G) = cell(G,i2,j2) or
    i1 = i2 & j1 = j2+1 & right_cell(f,k,G) = cell(G,i1-'1,j2)
     by A1,A2,A3,A4,A5,Def2;
   hence thesis by GOBRD11:33;
end;

theorem
    1 <= k & k+1 <= len f & f is_sequence_on G & k+1 <= n
   implies left_cell(f,k,G) = left_cell(f|n,k,G) &
      right_cell(f,k,G) = right_cell(f|n,k,G)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: k+1 <= n;
 per cases;
 suppose len f <= n;
  hence thesis by TOPREAL1:2;
 suppose
A4: n < len f;
  consider i1,j1,i2,j2 being Nat such that
A5:  [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A6:  [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A7:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,JORDAN8:6;
A8: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
   set lf = left_cell(f,k,G), lfn = left_cell(f|n,k,G),
       rf = right_cell(f,k,G), rfn = right_cell(f|n,k,G);
A9: f|n is_sequence_on G by A2,GOBOARD1:38;
A10: len(f|n) = n by A4,TOPREAL1:3;
   then k in dom(f|n) & k+1 in dom(f|n) by A1,A3,GOBOARD2:3;
then A11: (f|n)/.k = f/.k & (f|n)/.(k+1) = f/.(k+1) by TOPREAL1:1;
    now per cases by A7;
   suppose
A12:  i1 = i2 & j1+1 = j2;
    hence lf = cell(G,i1-'1,j1) by A1,A2,A5,A6,A8,Def3
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A12,Def3;
    thus rf = cell(G,i1,j1) by A1,A2,A5,A6,A8,A12,Def2
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A12,Def2;
   suppose
A13:  i1+1 = i2 & j1 = j2;
    hence lf = cell(G,i1,j1) by A1,A2,A5,A6,A8,Def3
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A13,Def3;
    thus rf = cell(G,i1,j1-'1) by A1,A2,A5,A6,A8,A13,Def2
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A13,Def2;
   suppose
A14:  i1 = i2+1 & j1 = j2;
    hence lf = cell(G,i2,j2-'1) by A1,A2,A5,A6,A8,Def3
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A14,Def3;
    thus rf = cell(G,i2,j2) by A1,A2,A5,A6,A8,A14,Def2
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A14,Def2;
   suppose
A15:  i1 = i2 & j1 = j2+1;
    hence lf = cell(G,i1,j2) by A1,A2,A5,A6,A8,Def3
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A15,Def3;
    thus rf = cell(G,i1-'1,j2) by A1,A2,A5,A6,A8,A15,Def2
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A15,Def2;
  end;
 hence thesis;
end;

theorem
    1 <= k & k+1 <= len(f/^n) & n <= len f & f is_sequence_on G
   implies left_cell(f,k+n,G) = left_cell(f/^n,k,G) &
      right_cell(f,k+n,G) = right_cell(f/^n,k,G)
 proof set g = (f/^n);
   assume that
A1:  1 <= k & k+1 <= len g and
A2: n <= len f and
A3:  f is_sequence_on G;
A4:  g is_sequence_on G by A3,JORDAN8:5;
  then consider i1,j1,i2,j2 being Nat such that
A5:  [i1,j1] in Indices G & g/.k = G*(i1,j1) and
A6:  [i2,j2] in Indices G & g/.(k+1) = G*(i2,j2) and
A7:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,JORDAN8:6;
A8: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
   set lf = left_cell(f,k+n,G), lfn = left_cell(g,k,G),
       rf = right_cell(f,k+n,G), rfn = right_cell(g,k,G);
A9: len g = len f - n by A2,RFINSEQ:def 2;
     k in dom g & k+1 in dom g by A1,GOBOARD2:3;
then A10: g/.k = f/.(k+n) & g/.(k+1) = f/.(k+1+n) by FINSEQ_5:30;
A11: k+1+n = k+n+1 by XCMPLX_1:1;
      k+1+n <= (len g)+n by A1,AXIOMS:24;
then A12: 1 <= k+n & k+1+n <= len f by A1,A9,NAT_1:37,XCMPLX_1:27;
    now per cases by A7;
   suppose
A13:  i1 = i2 & j1+1 = j2;
    hence lf = cell(G,i1-'1,j1) by A3,A5,A6,A8,A10,A11,A12,Def3
            .= lfn by A1,A4,A5,A6,A8,A13,Def3;
    thus rf = cell(G,i1,j1) by A3,A5,A6,A8,A10,A11,A12,A13,Def2
           .= rfn by A1,A4,A5,A6,A8,A13,Def2;
   suppose
A14:  i1+1 = i2 & j1 = j2;
    hence lf = cell(G,i1,j1) by A3,A5,A6,A8,A10,A11,A12,Def3
            .= lfn by A1,A4,A5,A6,A8,A14,Def3;
    thus rf = cell(G,i1,j1-'1) by A3,A5,A6,A8,A10,A11,A12,A14,Def2
           .= rfn by A1,A4,A5,A6,A8,A14,Def2;
   suppose
A15:  i1 = i2+1 & j1 = j2;
    hence lf = cell(G,i2,j2-'1) by A3,A5,A6,A8,A10,A11,A12,Def3
            .= lfn by A1,A4,A5,A6,A8,A15,Def3;
    thus rf = cell(G,i2,j2) by A3,A5,A6,A8,A10,A11,A12,A15,Def2
           .= rfn by A1,A4,A5,A6,A8,A15,Def2;
   suppose
A16:  i1 = i2 & j1 = j2+1;
    hence lf = cell(G,i1,j2) by A3,A5,A6,A8,A10,A11,A12,Def3
            .= lfn by A1,A4,A5,A6,A8,A16,Def3;
    thus rf = cell(G,i1-'1,j2) by A3,A5,A6,A8,A10,A11,A12,A16,Def2
           .= rfn by A1,A4,A5,A6,A8,A16,Def2;
  end;
 hence thesis;
 end;

theorem
    for G being Go-board, f being standard special_circular_sequence
    st 1 <= n & n+1 <= len f & f is_sequence_on G
  holds
    left_cell(f,n,G) c= left_cell(f,n) & right_cell(f,n,G) c= right_cell(f,n)
proof
  let G be Go-board,f be standard special_circular_sequence such that
A1: 1 <= n & n+1 <= len f and
A2: f is_sequence_on G;
  set F = GoB f;
A3: Values F c= Values G by A2,Th21;
   f is_sequence_on F by GOBOARD5:def 5;
  then consider m,k,i,j such that
A4:  [m,k] in Indices F and
A5:  f/.n = F*(m,k) and
A6:  [i,j] in Indices F and
A7:  f/.(n+1) = F*(i,j) and
       m = i & k+1 = j or m+1 = i & k = j or
      m = i+1 & k = j or m = i & k = j+1 by A1,JORDAN8:6;
A8:  1 <= m & m <= len F & 1 <= k & k <= width F by A4,GOBOARD5:1;
A9:  1 <= i & i <= len F & 1 <= j & j <= width F by A6,GOBOARD5:1;
then A10:  F*(i,j)`1 = F*(i,1)`1 & F*(i,k)`1 = F*(i,1)`1 by A8,GOBOARD5:3;
A11:  F*(i,j)`2 = F*(1,j)`2 & F*(m,j)`2 = F*(1,j)`2 by A8,A9,GOBOARD5:2;
   consider i1,j1,i2,j2 such that
A12:  [i1,j1] in Indices G and
A13:  f/.n = G*(i1,j1) and
A14:  [i2,j2] in Indices G and
A15:  f/.(n+1) = G*(i2,j2) and
A16:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,JORDAN8:6;
A17:  1 <= i1 & i1 <= len G & 1 <= j1 & j1 <= width G by A12,GOBOARD5:1;
A18:  1 <= i2 & i2 <= len G & 1 <= j2 & j2 <= width G by A14,GOBOARD5:1;
then A19:  G*(i1,j1)`1 = G*(i1,1)`1 & G*(i2,j2)`1 = G*(i2,1)`1 by A17,GOBOARD5:
3;
A20:  G*(i1,j1)`2 = G*(1,j1)`2 & G*(i2,j1)`2 = G*(1,j1)`2 by A17,A18,GOBOARD5:2
;
A21:  k+1 >= 1 & j+1 >= 1 & m+1 >= 1 & i+1 >= 1 by NAT_1:37;
A22:  k+1 > k & j+1 > j & m+1 > m & i+1 > i by NAT_1:38;
A23:  i1+1 > i1 & j1+1 > j1 & i2+1 > i2 & j2+1 > j2 by NAT_1:38;
   per cases by A16;
   suppose
A24:   i1 = i2 & j1+1 = j2;
       now assume j <= k;
then A25:    F*(i,j)`2 <= F*(m,k)`2 by A8,A9,A11,SPRECT_3:24;
        j1 < j2 by A24,NAT_1:38;
      hence contradiction by A5,A7,A13,A15,A17,A18,A20,A25,GOBOARD5:5;
     end;
then A26:   k+1 <= j by NAT_1:38;
       now assume
A27:    k+1 < j;
then A28:    k+1 < width F by A9,AXIOMS:22;
      then consider l,i' such that
A29:    l in dom f and
A30:    [i',k+1] in Indices F and
A31:    f/.l = F*(i',k+1) by A21,JORDAN5D:10;
      1 <= i' & i' <= len F by A30,GOBOARD5:1;
then A32:    F*(i',k+1)`2 = F*(1,k+1)`2 & F*(m,k+1)`2 = F*(1,k+1)`2
         by A8,A21,A28,GOBOARD5:2;
      consider i1',j1' such that
A33:    [i1',j1'] in Indices G and
A34:    f/.l = G*(i1',j1') by A2,A29,GOBOARD1:def 11;
A35:    1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A33,GOBOARD5:1;
then A36:    G*(i1',j1')`2 = G*(1,j1')`2 & G*(i1',j1)`2 = G*(1,j1)`2
         by A17,GOBOARD5:2;
A37:    G*(i2,j2)`2 = G*(1,j2)`2 & G*(i1',j2)`2 = G*(1,j2)`2
         by A18,A35,GOBOARD5:2;
A38:  now assume j1 >= j1';
then G*(i1',j1')`2 <= G*(i1,j1)`2 by A17,A20,A35,A36,SPRECT_3:24;
       hence contradiction by A5,A8,A13,A22,A28,A31,A32,A34,GOBOARD5:5;
      end;
        now assume j2 <= j1';
then G*(i2,j2)`2 <= G*(i1',j1')`2 by A18,A35,A37,SPRECT_3:24;
       hence contradiction by A7,A8,A9,A11,A15,A21,A27,A31,A32,A34,GOBOARD5:5;
      end;
      hence contradiction by A24,A38,NAT_1:38;
     end;
   then A39: k+1 = j by A26,AXIOMS:21;
   then A40: right_cell(f,n,G) = cell(G,i1,j1) & right_cell(f,n) = cell(F,m,k)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A24,Def2,GOBOARD5:def 6;
       left_cell(f,n,G) = cell(G,i1-'1,j1) & left_cell(f,n) = cell(F,m-'1,k)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A24,A39,Def3,GOBOARD5:def
7;
     hence thesis by A3,A4,A5,A12,A13,A40,Th18,Th19;
   suppose
A41:   i1+1 = i2 & j1 = j2;
       now assume i <= m;
then A42:    F*(i,j)`1 <= F*(m,k)`1 by A8,A9,A10,SPRECT_3:25;
        i1 < i2 by A41,NAT_1:38;
      hence contradiction by A5,A7,A13,A15,A17,A18,A41,A42,GOBOARD5:4;
     end;
then A43:   m+1 <= i by NAT_1:38;
       now assume
A44:    m+1 < i;
then A45:    m+1 < len F by A9,AXIOMS:22;
      then consider l,j' such that
A46:    l in dom f and
A47:    [m+1,j'] in Indices F and
A48:    f/.l = F*(m+1,j') by A21,JORDAN5D:9;
A49:    1 <= m+1 by NAT_1:37;
      1 <= j' & j' <= width F by A47,GOBOARD5:1;
then A50:    F*(m+1,j')`1 = F*(m+1,1)`1 & F*(m+1,k)`1 = F*(m+1,1)`1
         by A8,A21,A45,GOBOARD5:3;
A51:    F*(m+1,j)`1 = F*(m+1,1)`1 & F*(m+1,k)`1 = F*(m+1,1)`1
         by A8,A9,A21,A45,GOBOARD5:3;
      consider i1',j1' such that
A52:    [i1',j1'] in Indices G and
A53:    f/.l = G*(i1',j1') by A2,A46,GOBOARD1:def 11;
A54:    1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A52,GOBOARD5:1;
then A55:    G*(i1',j1')`1 = G*(i1',1)`1 & G*(i1',j1)`1 = G*(i1',1)`1
         by A17,GOBOARD5:3;
A56:    G*(i2,j2)`1 = G*(i2,1)`1 & G*(i2,j1')`1 = G*(i2,1)`1
         by A18,A54,GOBOARD5:3;
A57:  now assume i1 >= i1';
then G*(i1',j1')`1 <= G*(i1,j1)`1 by A17,A54,A55,SPRECT_3:25;
       hence contradiction by A5,A8,A13,A22,A45,A48,A50,A53,GOBOARD5:4;
      end;
        now assume i2 <= i1';
then G*(i2,j2)`1 <= G*(i1',j1')`1 by A18,A54,A56,SPRECT_3:25;
       hence contradiction by A7,A9,A15,A44,A48,A49,A50,A51,A53,GOBOARD5:4;
      end;
      hence contradiction by A41,A57,NAT_1:38;
     end;
   then A58: m+1 = i by A43,AXIOMS:21;
   then A59: right_cell(f,n,G) = cell(G,i1,j1-'1) & right_cell(f,n) = cell(F,m,
k-'1)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A41,Def2,GOBOARD5:def 6;
        left_cell(f,n,G) = cell(G,i1,j1) & left_cell(f,n) = cell(F,m,k)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A41,A58,Def3,GOBOARD5:def
7;
     hence thesis by A3,A4,A5,A12,A13,A59,Th18,Th20;
   suppose
A60:   i1 = i2+1 & j1 = j2;
       now assume m <= i;
then A61:    F*(i,j)`1 >= F*(m,k)`1 by A8,A9,A10,SPRECT_3:25;
        i1 > i2 by A60,NAT_1:38;
      hence contradiction by A5,A7,A13,A15,A17,A18,A60,A61,GOBOARD5:4;
     end;
then A62:   i+1 <= m by NAT_1:38;
       now assume
A63:    m > i+1;
then A64:    i+1 < len F by A8,AXIOMS:22;
      then consider l,j' such that
A65:    l in dom f and
A66:    [i+1,j'] in Indices F and
A67:    f/.l = F*(i+1,j') by A21,JORDAN5D:9;
A68:    1 <= i+1 by NAT_1:37;
      1 <= j' & j' <= width F by A66,GOBOARD5:1;
then A69:    F*(i+1,j')`1 = F*(i+1,1)`1 & F*(i+1,j)`1 = F*(i+1,1)`1
         by A9,A21,A64,GOBOARD5:3;
A70:    F*(i+1,j)`1 = F*(i+1,1)`1 & F*(i+1,k)`1 = F*(i+1,1)`1
         by A8,A9,A21,A64,GOBOARD5:3;
      consider i1',j1' such that
A71:    [i1',j1'] in Indices G and
A72:    f/.l = G*(i1',j1') by A2,A65,GOBOARD1:def 11;
A73:    1 <= i1' & i1' <= len G & 1 <= j1' & j1' <= width G by A71,GOBOARD5:1;
then A74:    G*(i1',j1')`1 = G*(i1',1)`1 & G*(i1',j1)`1 = G*(i1',1)`1
         by A17,GOBOARD5:3;
A75:    G*(i2,j2)`1 = G*(i2,1)`1 & G*(i2,j1')`1 = G*(i2,1)`1
         by A18,A73,GOBOARD5:3;
A76:  now assume i2 >= i1';
then G*(i2,j2)`1 >= G*(i1',j1')`1 by A18,A73,A75,SPRECT_3:25;
       hence contradiction by A7,A9,A15,A22,A64,A67,A69,A72,GOBOARD5:4;
      end;
        now assume i1 <= i1';
then G*(i1',j1')`1 >= G*(i1,j1)`1 by A17,A73,A74,SPRECT_3:25;
       hence contradiction by A5,A8,A13,A63,A67,A68,A69,A70,A72,GOBOARD5:4;
      end;
      hence contradiction by A60,A76,NAT_1:38;
     end;
   then A77: i+1 = m by A62,AXIOMS:21;
   then A78: right_cell(f,n,G) = cell(G,i2,j2) & right_cell(f,n) = cell(F,i,j)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A60,Def2,GOBOARD5:def 6;
       left_cell(f,n,G) = cell(G,i2,j2-'1) & left_cell(f,n) = cell(F,i,j-'1)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A60,A77,Def3,GOBOARD5:def
7;
     hence thesis by A3,A6,A7,A14,A15,A78,Th18,Th20;
   suppose
A79:  i1 = i2 & j1 = j2+1;
A80: now assume
A81:  m <> i;
     per cases by A81,REAL_1:def 5;
     suppose m < i;
      hence contradiction by A5,A7,A8,A9,A10,A13,A15,A19,A79,GOBOARD5:4;
     suppose m > i;
      hence contradiction by A5,A7,A8,A9,A10,A13,A15,A19,A79,GOBOARD5:4;
     end;
       now assume j >= k;
then A82:    F*(i,j)`2 >= F*(m,k)`2 by A8,A9,A11,SPRECT_3:24;
        j1 > j2 by A79,NAT_1:38;
      hence contradiction by A5,A7,A13,A15,A17,A18,A20,A82,GOBOARD5:5;
     end;
then A83:   j+1 <= k by NAT_1:38;
       now assume
A84:    j+1 < k;
then A85:    j+1 < width F by A8,AXIOMS:22;
      then consider l,i' such that
A86:    l in dom f and
A87:    [i',j+1] in Indices F and
A88:    f/.l = F*(i',j+1) by A21,JORDAN5D:10;
      1 <= i' & i' <= len F by A87,GOBOARD5:1;
then A89:    F*(i',j+1)`2 = F*(1,j+1)`2 & F*(i,j+1)`2 = F*(1,j+1)`2
         by A9,A21,A85,GOBOARD5:2;
A90:    F*(i,j+1)`2 = F*(1,j+1)`2 & F*(m,j+1)`2 = F*(1,j+1)`2
         by A8,A9,A21,A85,GOBOARD5:2;
      consider i1',j1' such that
A91:    [i1',j1'] in Indices G and
A92:    f/.l = G*(i1',j1') by A2,A86,GOBOARD1:def 11;
A93:    1 <= i1' & i1' <= len G & 1 <= j1' & j1' <=
 width G by A91,GOBOARD5:1;
then A94:    G*(i1',j1')`2 = G*(1,j1')`2 & G*(i1',j1)`2 = G*(1,j1)`2
         by A17,GOBOARD5:2;
A95:    G*(i2,j2)`2 = G*(1,j2)`2 & G*(i1',j2)`2 = G*(1,j2)`2
         by A18,A93,GOBOARD5:2;
A96: now assume j2 >= j1';
then G*(i2,j2)`2 >= G*(i1',j1')`2 by A18,A93,A95,SPRECT_3:24;
       hence contradiction by A7,A9,A15,A22,A85,A88,A89,A92,GOBOARD5:5;
      end;
        now assume j1 <= j1';
then G*(i1',j1')`2 >= G*(i1,j1)`2 by A17,A20,A93,A94,SPRECT_3:24;
       hence contradiction by A5,A8,A13,A21,A84,A88,A89,A90,A92,GOBOARD5:5;
      end;
      hence contradiction by A79,A96,NAT_1:38;
     end;
   then A97: j+1 = k by A83,AXIOMS:21;
   then A98: right_cell(f,n,G) = cell(G,i1-'1,j2) & right_cell(f,n) = cell(F,m
-'1,j)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A79,Def2,GOBOARD5:def 6;
       left_cell(f,n,G) = cell(G,i1,j2) & left_cell(f,n) = cell(F,m,j)
        by A1,A2,A4,A5,A6,A7,A12,A13,A14,A15,A22,A23,A79,A97,Def3,GOBOARD5:def
7;
     hence thesis by A3,A6,A7,A14,A15,A79,A80,A98,Th18,Th19;
 end;

definition let f,G,k;
  assume that
A1:  1 <= k & k+1 <= len f and
A2:  f is_sequence_on G;
   consider i1,j1,i2,j2 being Nat such that
A3:  [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A4:  [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A5:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,JORDAN8:6;
 func front_right_cell(f,k,G) -> Subset of TOP-REAL 2 means
 :Def4:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & it = cell(G,i2,j2) or
    i1+1 = i2 & j1 = j2 & it = cell(G,i2,j2-'1) or
    i1 = i2+1 & j1 = j2 & it = cell(G,i2-'1,j2) or
    i1 = i2 & j1 = j2+1 & it = cell(G,i2-'1,j2-'1);
 existence
  proof
   per cases by A5;
   suppose
A6:  i1 = i2 & j1+1 = j2;
     take cell(G,i2,j2);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A6;
   suppose
A7:  i1+1 = i2 & j1 = j2;
     take cell(G,i2,j2-'1);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A7;
   suppose
A8:  i1 = i2+1 & j1 = j2;
     take cell(G,i2-'1,j2);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A8;
   suppose
A9:  i1 = i2 & j1 = j2+1;
     take cell(G,i2-'1,j2-'1);
    let i1',j1',i2',j2' be Nat;
    assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
            f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
     then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
    hence thesis by A9;
  end;
 uniqueness
  proof let P1,P2 be Subset of TOP-REAL 2 such that
A10: for i1,j1,i2,j2 being Nat st
      [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
    i1 = i2 & j1+1 = j2 & P1 = cell(G,i2,j2) or
    i1+1 = i2 & j1 = j2 & P1 = cell(G,i2,j2-'1) or
    i1 = i2+1 & j1 = j2 & P1 = cell(G,i2-'1,j2) or
    i1 = i2 & j1 = j2+1 & P1 = cell(G,i2-'1,j2-'1) and
A11:  for i1,j1,i2,j2 being Nat st
      [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
    i1 = i2 & j1+1 = j2 & P2 = cell(G,i2,j2) or
    i1+1 = i2 & j1 = j2 & P2 = cell(G,i2,j2-'1) or
    i1 = i2+1 & j1 = j2 & P2 = cell(G,i2-'1,j2) or
    i1 = i2 & j1 = j2+1 & P2 = cell(G,i2-'1,j2-'1);
   per cases by A5;
   suppose i1 = i2 & j1+1 = j2;
then A12: j1 < j2 by REAL_1:69;
A13: j2 <= j2+1 by NAT_1:29;
   hence P1 = cell(G,i2,j2) by A3,A4,A10,A12 .= P2 by A3,A4,A11,A12,A13;
   suppose i1+1 = i2 & j1 = j2;
then A14: i1 < i2 by REAL_1:69;
A15: i2 <= i2+1 by NAT_1:29;
   hence P1 = cell(G,i2,j2-'1) by A3,A4,A10,A14 .= P2 by A3,A4,A11,A14,A15;
   suppose i1 = i2+1 & j1 = j2;
then A16: i2 < i1 by REAL_1:69;
A17: i1 <= i1+1 by NAT_1:29;
   hence P1 = cell(G,i2-'1,j2) by A3,A4,A10,A16 .= P2 by A3,A4,A11,A16,A17;
   suppose i1 = i2 & j1 = j2+1;
then A18: j2 < j1 by REAL_1:69;
A19: j1 <= j1+1 by NAT_1:29;
   hence P1 = cell(G,i2-'1,j2-'1) by A3,A4,A10,A18 .= P2 by A3,A4,A11,A18,A19;
  end;

 func front_left_cell(f,k,G) -> Subset of TOP-REAL 2 means
 :Def5:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & it = cell(G,i2-'1,j2) or
    i1+1 = i2 & j1 = j2 & it = cell(G,i2,j2) or
    i1 = i2+1 & j1 = j2 & it = cell(G,i2-'1,j2-'1) or
    i1 = i2 & j1 = j2+1 & it = cell(G,i2,j2-'1);
  existence
   proof
    per cases by A5;
    suppose
 A20:  i1 = i2 & j1+1 = j2;
     take cell(G,i2-'1,j2);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A20;
    suppose
 A21:  i1+1 = i2 & j1 = j2;
     take cell(G,i2,j2);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A21;
    suppose
 A22:  i1 = i2+1 & j1 = j2;
     take cell(G,i2-'1,j2-'1);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A22;
    suppose
 A23:  i1 = i2 & j1 = j2+1;
     take cell(G,i2,j2-'1);
     let i1',j1',i2',j2' be Nat;
     assume [i1',j1'] in Indices G & [i2',j2'] in Indices G &
             f/.k = G*(i1',j1') & f/.(k+1) = G*(i2',j2');
      then i1 = i1' & i2 = i2' & j1 = j1' & j2 = j2' by A3,A4,GOBOARD1:21;
     hence thesis by A23;
   end;
  uniqueness
   proof let P1,P2 be Subset of TOP-REAL 2 such that
 A24: for i1,j1,i2,j2 being Nat st
      [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
    i1 = i2 & j1+1 = j2 & P1 = cell(G,i2-'1,j2) or
    i1+1 = i2 & j1 = j2 & P1 = cell(G,i2,j2) or
    i1 = i2+1 & j1 = j2 & P1 = cell(G,i2-'1,j2-'1) or
    i1 = i2 & j1 = j2+1 & P1 = cell(G,i2,j2-'1) and
 A25: for i1,j1,i2,j2 being Nat st
      [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2) holds
    i1 = i2 & j1+1 = j2 & P2 = cell(G,i2-'1,j2) or
    i1+1 = i2 & j1 = j2 & P2 = cell(G,i2,j2) or
    i1 = i2+1 & j1 = j2 & P2 = cell(G,i2-'1,j2-'1) or
    i1 = i2 & j1 = j2+1 & P2 = cell(G,i2,j2-'1);
    per cases by A5;
    suppose i1 = i2 & j1+1 = j2;
then A26:  j1 < j2 by REAL_1:69;
A27:  j2 <= j2+1 by NAT_1:29;
    hence P1 = cell(G,i2-'1,j2) by A3,A4,A24,A26 .= P2 by A3,A4,A25,A26,A27;
    suppose i1+1 = i2 & j1 = j2;
then A28:  i1 < i2 by REAL_1:69;
A29:  i2 <= i2+1 by NAT_1:29;
    hence P1 = cell(G,i2,j2) by A3,A4,A24,A28 .= P2 by A3,A4,A25,A28,A29;
    suppose i1 = i2+1 & j1 = j2;
then A30:  i2 < i1 by REAL_1:69;
A31:  i1 <= i1+1 by NAT_1:29;
    hence P1 = cell(G,i2-'1,j2-'1) by A3,A4,A24,A30
            .= P2 by A3,A4,A25,A30,A31;
    suppose i1 = i2 & j1 = j2+1;
then A32:  j2 < j1 by REAL_1:69;
A33:  j1 <= j1+1 by NAT_1:29;
    hence P1 = cell(G,i2,j2-'1) by A3,A4,A24,A32
            .= P2 by A3,A4,A25,A32,A33;
   end;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i,j+1] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1)
  implies front_left_cell(f,k,G) = cell(G,i-'1,j+1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i,j+1] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i,j+1);
A6: j < j+1 by REAL_1:69;
    j+1 <= j+1+1 by NAT_1:29;
  hence front_left_cell(f,k,G) = cell(G,i-'1,j+1) by A1,A2,A3,A4,A5,A6,Def5;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i,j+1] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i,j+1)
  implies front_right_cell(f,k,G) = cell(G,i,j+1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i,j+1] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i,j+1);
A6: j < j+1 by REAL_1:69;
    j+1 <= j+1+1 by NAT_1:29;
 hence front_right_cell(f,k,G) = cell(G,i,j+1) by A1,A2,A3,A4,A5,A6,Def4;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j)
  implies front_left_cell(f,k,G) = cell(G,i+1,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i+1,j);
A6: i < i+1 by REAL_1:69;
   i+1 <= i+1+1 by NAT_1:29;
 hence front_left_cell(f,k,G) = cell(G,i+1,j) by A1,A2,A3,A4,A5,A6,Def5;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i,j) & f/.(k+1) = G*(i+1,j)
  implies front_right_cell(f,k,G) = cell(G,i+1,j-'1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i,j) and
A5: f/.(k+1) = G*(i+1,j);
A6: i < i+1 by REAL_1:69;
     i+1 <= i+1+1 by NAT_1:29;
hence front_right_cell(f,k,G) = cell(G,i+1,j-'1) by A1,A2,A3,A4,A5,A6,Def4;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j)
  implies front_left_cell(f,k,G) = cell(G,i-'1,j-'1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i+1,j) and
A5: f/.(k+1) = G*(i,j);
A6: i < i+1 by REAL_1:69;
   i+1 <= i+1+1 by NAT_1:29;
 hence front_left_cell(f,k,G) = cell(G,i-'1,j-'1) by A1,A2,A3,A4,A5,A6,Def5;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j] in Indices G & [i+1,j] in Indices G &
 f/.k = G*(i+1,j) & f/.(k+1) = G*(i,j)
  implies front_right_cell(f,k,G) = cell(G,i-'1,j)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j] in Indices G & [i+1,j] in Indices G and
A4: f/.k = G*(i+1,j) and
A5: f/.(k+1) = G*(i,j);
A6: i < i+1 by REAL_1:69;
     i+1 <= i+1+1 by NAT_1:29;
   hence front_right_cell(f,k,G) = cell(G,i-'1,j) by A1,A2,A3,A4,A5,A6,Def4;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j+1] in Indices G & [i,j] in Indices G &
 f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j)
  implies front_left_cell(f,k,G) = cell(G,i,j-'1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j+1] in Indices G & [i,j] in Indices G and
A4: f/.k = G*(i,j+1) and
A5: f/.(k+1) = G*(i,j);
A6: j < j+1 by REAL_1:69;
   j+1 <= j+1+1 by NAT_1:29;
 hence front_left_cell(f,k,G) = cell(G,i,j-'1) by A1,A2,A3,A4,A5,A6,Def5;
end;

theorem
   1 <= k & k+1 <= len f & f is_sequence_on G &
 [i,j+1] in Indices G & [i,j] in Indices G &
 f/.k = G*(i,j+1) & f/.(k+1) = G*(i,j)
   implies front_right_cell(f,k,G) = cell(G,i-'1,j-'1)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: [i,j+1] in Indices G & [i,j] in Indices G and
A4: f/.k = G*(i,j+1) and
A5: f/.(k+1) = G*(i,j);
A6: j < j+1 by REAL_1:69;
     j+1 <= j+1+1 by NAT_1:29;
   hence front_right_cell(f,k,G) = cell(G,i-'1,j-'1) by A1,A2,A3,A4,A5,A6,Def4
;
end;

theorem
    1 <= k & k+1 <= len f & f is_sequence_on G & k+1 <= n
   implies front_left_cell(f,k,G) = front_left_cell(f|n,k,G) &
      front_right_cell(f,k,G) = front_right_cell(f|n,k,G)
proof assume that
A1: 1 <= k & k+1 <= len f and
A2: f is_sequence_on G and
A3: k+1 <= n;
 per cases;
 suppose len f <= n;
  hence thesis by TOPREAL1:2;
 suppose
A4: n < len f;
  consider i1,j1,i2,j2 being Nat such that
A5:  [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A6:  [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A7:  i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A1,A2,JORDAN8:6;
A8: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
   set lf = front_left_cell(f,k,G), lfn = front_left_cell(f|n,k,G),
       rf = front_right_cell(f,k,G), rfn = front_right_cell(f|n,k,G);
A9: f|n is_sequence_on G by A2,GOBOARD1:38;
A10: len(f|n) = n by A4,TOPREAL1:3;
   then k in dom(f|n) & k+1 in dom(f|n) by A1,A3,GOBOARD2:3;
then A11: (f|n)/.k = f/.k & (f|n)/.(k+1) = f/.(k+1) by TOPREAL1:1;
    now per cases by A7;
   suppose
A12:  i1 = i2 & j1+1 = j2;
    hence lf = cell(G,i2-'1,j2) by A1,A2,A5,A6,A8,Def5
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A12,Def5;
    thus rf = cell(G,i2,j2) by A1,A2,A5,A6,A8,A12,Def4
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A12,Def4;
   suppose
A13:  i1+1 = i2 & j1 = j2;
    hence lf = cell(G,i2,j2) by A1,A2,A5,A6,A8,Def5
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A13,Def5;
    thus rf = cell(G,i2,j2-'1) by A1,A2,A5,A6,A8,A13,Def4
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A13,Def4;
   suppose
A14:  i1 = i2+1 & j1 = j2;
    hence lf = cell(G,i2-'1,j2-'1) by A1,A2,A5,A6,A8,Def5
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A14,Def5;
    thus rf = cell(G,i2-'1,j2) by A1,A2,A5,A6,A8,A14,Def4
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A14,Def4;
   suppose
A15:  i1 = i2 & j1 = j2+1;
    hence lf = cell(G,i2,j2-'1) by A1,A2,A5,A6,A8,Def5
            .= lfn by A1,A3,A5,A6,A8,A9,A10,A11,A15,Def5;
    thus rf = cell(G,i2-'1,j2-'1) by A1,A2,A5,A6,A8,A15,Def4
           .= rfn by A1,A3,A5,A6,A8,A9,A10,A11,A15,Def4;
  end;
 hence thesis;
end;

definition let D be set; let f be FinSequence of D, G be (Matrix of D), k;
 pred f turns_right k,G means
 :Def6:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & [i2+1,j2] in Indices G & f/.(k+2) = G*(i2+1,j2) or
    i1+1 = i2 & j1 = j2 & [i2,j2-'1] in Indices G & f/.(k+2) = G*
(i2,j2-'1) or
    i1 = i2+1 & j1 = j2 & [i2,j2+1] in Indices G & f/.(k+2) = G*(i2,j2+1) or
    i1 = i2 & j1 = j2+1 & [i2-'1,j2] in Indices G & f/.(k+2) = G*(i2-'1,j2);

 pred f turns_left k,G means
 :Def7:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & [i2-'1,j2] in Indices G & f/.(k+2) = G*
(i2-'1,j2) or
    i1+1 = i2 & j1 = j2 & [i2,j2+1] in Indices G & f/.(k+2) = G*(i2,j2+1) or
    i1 = i2+1 & j1 = j2 & [i2,j2-'1] in Indices G & f/.(k+2) = G*
(i2,j2-'1) or
    i1 = i2 & j1 = j2+1 & [i2+1,j2] in Indices G & f/.(k+2) = G*(i2+1,j2);

 pred f goes_straight k,G means
 :Def8:
   for i1,j1,i2,j2 being Nat
    st [i1,j1] in Indices G & [i2,j2] in Indices G &
      f/.k = G*(i1,j1) & f/.(k+1) = G*(i2,j2)
   holds
    i1 = i2 & j1+1 = j2 & [i2,j2+1] in Indices G & f/.(k+2) = G*(i2,j2+1) or
    i1+1 = i2 & j1 = j2 & [i2+1,j2] in Indices G & f/.(k+2) = G*(i2+1,j2) or
    i1 = i2+1 & j1 = j2 & [i2-'1,j2] in Indices G & f/.(k+2) = G*
(i2-'1,j2) or
    i1 = i2 & j1 = j2+1 & [i2,j2-'1] in Indices G & f/.(k+2) = G*(i2,j2-'1);
end;

reserve D for set,
        f,f1,f2 for FinSequence of D,
        G for Matrix of D;

theorem
    1 <= k & k+2 <= len f & k+2 <= n
   & f|n turns_right k,G implies f turns_right k,G
proof assume that
A1: 1 <= k & k+2 <= len f and
A2: k+2 <= n and
A3: f|n turns_right k,G;
 per cases;
 suppose len f <= n;
  hence thesis by A3,TOPREAL1:2;
 suppose n < len f;
then len(f|n) = n by TOPREAL1:3;
   then k in dom(f|n) & k+1 in dom(f|n) & k+2 in dom(f|n)
    by A1,A2,GOBOARD2:4;
then A4:  (f|n)/.k = f/.k & (f|n)/.(k+1) = f/.(k+1) & (f|n)/.(k+2) = f/.(k+2)
      by TOPREAL1:1;
  let i1',j1',i2',j2' be Nat;
  thus thesis by A3,A4,Def6;
end;

theorem
    1 <= k & k+2 <= len f & k+2 <= n
   & f|n turns_left k,G implies f turns_left k,G
proof assume that
A1: 1 <= k & k+2 <= len f and
A2: k+2 <= n and
A3: f|n turns_left k,G;
 per cases;
 suppose len f <= n;
  hence thesis by A3,TOPREAL1:2;
 suppose n < len f;
then len(f|n) = n by TOPREAL1:3;
   then k in dom(f|n) & k+1 in dom(f|n) & k+2 in dom(f|n)
     by A1,A2,GOBOARD2:4;
then A4:  (f|n)/.k = f/.k & (f|n)/.(k+1) = f/.(k+1) & (f|n)/.(k+2) = f/.(k+2)
      by TOPREAL1:1;
  let i1',j1',i2',j2' be Nat;
  thus thesis by A3,A4,Def7;
end;

theorem
    1 <= k & k+2 <= len f & k+2 <= n
   & f|n goes_straight k,G implies f goes_straight k,G
proof assume that
A1: 1 <= k & k+2 <= len f and
A2: k+2 <= n and
A3: f|n goes_straight k,G;
 per cases;
 suppose len f <= n;
  hence thesis by A3,TOPREAL1:2;
 suppose n < len f;
 then len(f|n) = n by TOPREAL1:3;
   then k in dom(f|n) & k+1 in dom(f|n) & k+2 in dom(f|n)
    by A1,A2,GOBOARD2:4;
then A4:  (f|n)/.k = f/.k & (f|n)/.(k+1) = f/.(k+1) & (f|n)/.(k+2) = f/.(k+2)
      by TOPREAL1:1;
  let i1',j1',i2',j2' be Nat;
  thus thesis by A3,A4,Def8;
end;

theorem
   1 < k & k+1 <= len f1 & k+1 <= len f2 &
 f1 is_sequence_on G &
 f1|k = f2|k & f1 turns_right k-'1,G & f2 turns_right k-'1,G
  implies f1|(k+1) = f2|(k+1)
proof assume that
A1: 1 < k & k+1 <= len f1 and
A2: k+1 <= len f2 and
A3: f1 is_sequence_on G and
A4: f1|k = f2|k and
A5: f1 turns_right k-'1,G and
A6: f2 turns_right k-'1,G;
A7: 1 <= k-'1 by A1,JORDAN3:12;
A8: k = k-'1+1 by A1,AMI_5:4;
    k <= k+1 by NAT_1:37;
then A9: k <= len f1 & k <= len f2 by A1,A2,AXIOMS:22;
then A10: k <= len(f1|k) by TOPREAL1:3;
    k-'1 <= k by GOBOARD9:2;
  then k-'1 <= len(f1|k) by A9,TOPREAL1:3;
then A11: k-'1 in dom(f1|k) & k in dom(f1|k) by A1,A7,A10,FINSEQ_3:27;
then A12: f1/.(k-'1) = (f1|k)/.(k-'1) & f1/.k = (f1|k)/.k by TOPREAL1:1;
A13: f2/.(k-'1) = (f2|k)/.(k-'1) & f2/.k = (f2|k)/.k by A4,A11,TOPREAL1:1;
A14: k+1 = k-'1+(1+1) by A8,XCMPLX_1:1;
 consider i1,j1,i2,j2 being Nat such that
A15: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) and
A16: [i2,j2] in Indices G & f1/.k = G*(i2,j2) and
A17: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A3,A7,A8,A9,JORDAN8:6;
A18: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
   now per cases by A17;
  suppose
A19:  i1 = i2 & j1+1 = j2;
   hence f1/.(k+1) = G*(i2+1,j2) by A5,A8,A14,A15,A16,A18,Def6
                 .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A19,Def6;
  suppose
A20:  i1+1 = i2 & j1 = j2;
   hence f1/.(k+1) = G*(i2,j2-'1) by A5,A8,A14,A15,A16,A18,Def6
                 .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A20,Def6;
  suppose
A21:  i1 = i2+1 & j1 = j2;
   hence f1/.(k+1) = G*(i2,j2+1) by A5,A8,A14,A15,A16,A18,Def6
                  .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A21,Def6;
  suppose
A22:  i1 = i2 & j1 = j2+1;
   hence f1/.(k+1) = G*(i2-'1,j2) by A5,A8,A14,A15,A16,A18,Def6
                  .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A22,Def6;
 end;
 hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A1,A4,JORDAN8:2
               .= f2|(k+1) by A2,JORDAN8:2;
end;

theorem
    1 < k & k+1 <= len f1 & k+1 <= len f2 &
  f1 is_sequence_on G &
  f1|k = f2|k & f1 turns_left k-'1,G & f2 turns_left k-'1,G
   implies f1|(k+1) = f2|(k+1)
proof assume that
A1: 1 < k & k+1 <= len f1 and
A2: k+1 <= len f2 and
A3: f1 is_sequence_on G and
A4: f1|k = f2|k and
A5: f1 turns_left k-'1,G and
A6: f2 turns_left k-'1,G;
A7: 1 <= k-'1 by A1,JORDAN3:12;
A8: k = k-'1+1 by A1,AMI_5:4;
    k <= k+1 by NAT_1:37;
then A9: k <= len f1 & k <= len f2 by A1,A2,AXIOMS:22;
then A10: k <= len(f1|k) by TOPREAL1:3;
    k-'1 <= k by GOBOARD9:2;
  then k-'1 <= len(f1|k) by A9,TOPREAL1:3;
then A11: k-'1 in dom(f1|k) & k in dom(f1|k) by A1,A7,A10,FINSEQ_3:27;
then A12: f1/.(k-'1) = (f1|k)/.(k-'1) & f1/.k = (f1|k)/.k by TOPREAL1:1;
A13: f2/.(k-'1) = (f2|k)/.(k-'1) & f2/.k = (f2|k)/.k by A4,A11,TOPREAL1:1;
A14: k+1 = k-'1+(1+1) by A8,XCMPLX_1:1;
 consider i1,j1,i2,j2 being Nat such that
A15: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) and
A16: [i2,j2] in Indices G & f1/.k = G*(i2,j2) and
A17: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A3,A7,A8,A9,JORDAN8:6;
A18: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
   now per cases by A17;
  suppose
A19:  i1 = i2 & j1+1 = j2;
   hence f1/.(k+1) = G*(i2-'1,j2) by A5,A8,A14,A15,A16,A18,Def7
                 .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A19,Def7;
  suppose
A20:  i1+1 = i2 & j1 = j2;
   hence f1/.(k+1) = G*(i2,j2+1) by A5,A8,A14,A15,A16,A18,Def7
                 .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A20,Def7;
  suppose
A21:  i1 = i2+1 & j1 = j2;
   hence f1/.(k+1) = G*(i2,j2-'1) by A5,A8,A14,A15,A16,A18,Def7
                  .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A21,Def7;
  suppose
A22:  i1 = i2 & j1 = j2+1;
   hence f1/.(k+1) = G*(i2+1,j2) by A5,A8,A14,A15,A16,A18,Def7
                  .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A22,Def7;
 end;
 hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A1,A4,JORDAN8:2
               .= f2|(k+1) by A2,JORDAN8:2;
end;

theorem
    1 < k & k+1 <= len f1 & k+1 <= len f2 &
  f1 is_sequence_on G &
  f1|k = f2|k & f1 goes_straight k-'1,G & f2 goes_straight k-'1,G
   implies f1|(k+1) = f2|(k+1)
proof assume that
A1: 1 < k & k+1 <= len f1 and
A2: k+1 <= len f2 and
A3: f1 is_sequence_on G and
A4: f1|k = f2|k and
A5: f1 goes_straight k-'1,G and
A6: f2 goes_straight k-'1,G;
A7: 1 <= k-'1 by A1,JORDAN3:12;
A8: k = k-'1+1 by A1,AMI_5:4;
    k <= k+1 by NAT_1:37;
then A9: k <= len f1 & k <= len f2 by A1,A2,AXIOMS:22;
then A10: k <= len(f1|k) by TOPREAL1:3;
    k-'1 <= k by GOBOARD9:2;
  then k-'1 <= len(f1|k) by A9,TOPREAL1:3;
then A11: k-'1 in dom(f1|k) & k in dom(f1|k) by A1,A7,A10,FINSEQ_3:27;
then A12: f1/.(k-'1) = (f1|k)/.(k-'1) & f1/.k = (f1|k)/.k by TOPREAL1:1;
A13: f2/.(k-'1) = (f2|k)/.(k-'1) & f2/.k = (f2|k)/.k by A4,A11,TOPREAL1:1;
A14: k+1 = k-'1+(1+1) by A8,XCMPLX_1:1;
 consider i1,j1,i2,j2 being Nat such that
A15: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) and
A16: [i2,j2] in Indices G & f1/.k = G*(i2,j2) and
A17: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or
      i1 = i2+1 & j1 = j2 or i1 = i2 & j1 = j2+1 by A3,A7,A8,A9,JORDAN8:6;
A18: i1+1 > i1 & i2+1 > i2 & j1+1 > j1 & j2+1 > j2 by NAT_1:38;
   now per cases by A17;
  suppose
A19:  i1 = i2 & j1+1 = j2;
   hence f1/.(k+1) = G*(i2,j2+1) by A5,A8,A14,A15,A16,A18,Def8
                 .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A19,Def8;
  suppose
A20:  i1+1 = i2 & j1 = j2;
   hence f1/.(k+1) = G*(i2+1,j2) by A5,A8,A14,A15,A16,A18,Def8
                 .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A20,Def8;
  suppose
A21:  i1 = i2+1 & j1 = j2;
   hence f1/.(k+1) = G*(i2-'1,j2) by A5,A8,A14,A15,A16,A18,Def8
                  .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A21,Def8;
  suppose
A22:  i1 = i2 & j1 = j2+1;
   hence f1/.(k+1) = G*(i2,j2-'1) by A5,A8,A14,A15,A16,A18,Def8
                  .= f2/.(k+1) by A4,A6,A8,A12,A13,A14,A15,A16,A18,A22,Def8;
 end;
 hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A1,A4,JORDAN8:2
               .= f2|(k+1) by A2,JORDAN8:2;
end;

theorem
    for D being non empty set, M being Matrix of D st
   1 <= i & i <= len M & 1 <= j & j <= width M holds
    M*(i,j) in Values M by Lm1;


Back to top