GOBRD13

:: Some Properties of Cells on Go Board
::  by Czes{\l}aw Byli\'nski
::
:: Received April 23, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, REAL_1, XBOOLE_0, FINSEQ_1, EUCLID, FUNCT_1,
      RELAT_1, TARSKI, NAT_1, MATRIX_1, TREES_1, XXREAL_0, CARD_1, GOBOARD1,
      PARTFUN1, ARYTM_3, MCART_1, ARYTM_1, GOBOARD5, GOBOARD2, PRE_TOPC,
      RLTOPSP1, COMPLEX1, RCOMP_1, RFINSEQ, ORDINAL4, GOBRD13;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, NAT_1, COMPLEX1, NAT_D, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
      FINSEQ_2, RFINSEQ, XXREAL_0, SEQ_4, STRUCT_0, MATRIX_0, MATRIX_1,
      PRE_TOPC, RLTOPSP1, EUCLID, TOPREAL1, GOBOARD1, GOBOARD2, GOBOARD5;
 constructors RFINSEQ, NAT_D, GOBOARD2, GOBOARD5, REAL_1, GOBOARD1, RELSET_1,
      SEQ_4, RVSUM_1;
 registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, FINSEQ_1, STRUCT_0,
      EUCLID, GOBOARD2, GOBOARD5, VALUED_0, SEQ_4, NAT_1, MATRIX_0;
 requirements NUMERALS, REAL, SUBSET, ARITHM;
 definitions TARSKI;
 theorems NAT_1, FINSEQ_1, MATRIX_0, GOBOARD1, EUCLID, FINSEQ_3, FINSEQ_5,
      TOPREAL1, GOBOARD5, ABSVALUE, FUNCT_1, FINSEQ_2, GOBRD11, GOBOARD2,
      SPRECT_3, JORDAN5D, FINSEQ_4, RFINSEQ, JORDAN8, PARTFUN2, XREAL_1,
      XXREAL_0, NAT_D, SEQM_3, SEQ_4;

begin

reserve i,i1,i2,i9,i19,j,j1,j2,j9,j19,k,k1,k2,l,m,n for Nat;
reserve r,s,r9,s9 for Real;
reserve D for non empty set, f for FinSequence of D;
reserve f for FinSequence of TOP-REAL 2, G for Go-board;

::$CT 7

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 object;
  assume y in rng f;
  then consider n being Element of NAT such that
A2: n in dom f and
A3: f/.n = y by PARTFUN2:2;
  ex i,j st [i,j] in Indices G & f/.n = G*(i,j) by A1,A2,GOBOARD1:def 9;
  then y in { G*(i,j): [i,j] in Indices G } by A3;
  hence thesis by MATRIX_0:39;
end;

theorem Th2:
  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);
  set p = G1*(1,j1);
A5: 1 <= j1 & j1 <= width G1 by A2,MATRIX_0:32;
  assume
A6: i1 <> 1;
  1 <= i1 by A2,MATRIX_0:32;
  then
A7: 1 < i1 by A6,XXREAL_0:1;
  i1 <= len G1 by A2,MATRIX_0:32;
  then
A8: p`1 < G1*(i1,j1)`1 by A5,A7,GOBOARD5:3;
  0 <> len G1 by MATRIX_0:def 10;
  then 1 <= len G1 by NAT_1:14;
  then [1,j1] in Indices G1 by A5,MATRIX_0:30;
  then p in {G1*(i,j): [i,j] in Indices G1};
  then p in Values G1 by MATRIX_0:39;
  then p in Values G2 by A1;
  then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
  then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= j & j <= width G2 by A10,MATRIX_0:32;
  0 <> len G2 by MATRIX_0:def 10;
  then
A12: 1 <= len G2 by NAT_1:14;
  then
A13: G2*(1,j)`1 = G2*(1,1)`1 by A11,GOBOARD5:2
    .= G2*(1,j2)`1 by A3,A12,GOBOARD5:2;
A14: i <= len G2 by A10,MATRIX_0:32;
  1 <= i by A10,MATRIX_0:32;
  then 1 < i by A4,A8,A9,A13,XXREAL_0:1;
  hence contradiction by A4,A8,A9,A14,A11,A13,GOBOARD5:3;
end;

theorem Th3:
  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);
  set p = G1*(len G1,j1);
A5: 1 <= j1 & j1 <= width G1 by A2,MATRIX_0:32;
  assume
A6: i1 <> len G1;
  i1 <= len G1 by A2,MATRIX_0:32;
  then
A7: i1 < len G1 by A6,XXREAL_0:1;
  1 <= i1 by A2,MATRIX_0:32;
  then
A8: G1*(i1,j1)`1 < p`1 by A5,A7,GOBOARD5:3;
  0 <> len G1 by MATRIX_0:def 10;
  then 1 <= len G1 by NAT_1:14;
  then [len G1,j1] in Indices G1 by A5,MATRIX_0:30;
  then p in {G1*(i,j): [i,j] in Indices G1};
  then p in Values G1 by MATRIX_0:39;
  then p in Values G2 by A1;
  then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
  then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= j & j <= width G2 by A10,MATRIX_0:32;
  0 <> len G2 by MATRIX_0:def 10;
  then
A12: 1 <= len G2 by NAT_1:14;
  then
A13: G2*(len G2,j)`1 = G2*(len G2,1)`1 by A11,GOBOARD5:2
    .= G2*(len G2,j2)`1 by A3,A12,GOBOARD5:2;
A14: 1 <= i by A10,MATRIX_0:32;
  i <= len G2 by A10,MATRIX_0:32;
  then i < len G2 by A4,A8,A9,A13,XXREAL_0:1;
  hence contradiction by A4,A8,A9,A14,A11,A13,GOBOARD5:3;
end;

theorem Th4:
  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);
  set p = G1*(i1,1);
A5: 1 <= i1 & i1 <= len G1 by A2,MATRIX_0:32;
  assume
A6: j1 <> 1;
  1 <= j1 by A2,MATRIX_0:32;
  then
A7: 1 < j1 by A6,XXREAL_0:1;
  j1 <= width G1 by A2,MATRIX_0:32;
  then
A8: p`2 < G1*(i1,j1)`2 by A5,A7,GOBOARD5:4;
  0 <> width G1 by MATRIX_0:def 10;
  then 1 <= width G1 by NAT_1:14;
  then [i1,1] in Indices G1 by A5,MATRIX_0:30;
  then p in {G1*(i,j): [i,j] in Indices G1};
  then p in Values G1 by MATRIX_0:39;
  then p in Values G2 by A1;
  then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
  then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 by A10,MATRIX_0:32;
  0 <> width G2 by MATRIX_0:def 10;
  then
A12: 1 <= width G2 by NAT_1:14;
  then
A13: G2*(i,1)`2 = G2*(1,1)`2 by A11,GOBOARD5:1
    .= G2*(i2,1)`2 by A3,A12,GOBOARD5:1;
A14: j <= width G2 by A10,MATRIX_0:32;
  1 <= j by A10,MATRIX_0:32;
  then 1 < j by A4,A8,A9,A13,XXREAL_0:1;
  hence contradiction by A4,A8,A9,A11,A14,A13,GOBOARD5:4;
end;

theorem Th5:
  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);
  set p = G1*(i1,width G1);
A5: 1 <= i1 & i1 <= len G1 by A2,MATRIX_0:32;
  assume
A6: j1 <> width G1;
  j1 <= width G1 by A2,MATRIX_0:32;
  then
A7: j1 < width G1 by A6,XXREAL_0:1;
  1 <= j1 by A2,MATRIX_0:32;
  then
A8: G1*(i1,j1)`2 < p`2 by A5,A7,GOBOARD5:4;
  0 <> width G1 by MATRIX_0:def 10;
  then 1 <= width G1 by NAT_1:14;
  then [i1,width G1] in Indices G1 by A5,MATRIX_0:30;
  then p in {G1*(i,j): [i,j] in Indices G1};
  then p in Values G1 by MATRIX_0:39;
  then p in Values G2 by A1;
  then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
  then consider i,j such that
A9: p = G2*(i,j) and
A10: [i,j] in Indices G2;
A11: 1 <= i & i <= len G2 by A10,MATRIX_0:32;
  0 <> width G2 by MATRIX_0:def 10;
  then
A12: 1 <= width G2 by NAT_1:14;
  then
A13: G2*(i,width G2)`2 = G2*(1,width G2)`2 by A11,GOBOARD5:1
    .= G2*(i2,width G2)`2 by A3,A12,GOBOARD5:1;
A14: 1 <= j by A10,MATRIX_0:32;
  j <= width G2 by A10,MATRIX_0:32;
  then j < width G2 by A4,A8,A9,A13,XXREAL_0:1;
  hence contradiction by A4,A8,A9,A11,A14,A13,GOBOARD5:4;
end;

theorem Th6:
  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 and
A3: i1 < len G1 and
A4: 1 <= j1 & j1 <= width G1 and
A5: 1 <= i2 and
A6: i2 < len G2 and
A7: 1 <= j2 & j2 <= width G2 and
A8: G1*(i1,j1) = G2*(i2,j2);
  set p = G1*(i1+1,j1);
A9: i1+1 <= len G1 by A3,NAT_1:13;
  1 <= i1+1 by A2,NAT_1:13;
  then [i1+1,j1] in Indices G1 by A4,A9,MATRIX_0:30;
  then p in {G1*(i,j): [i,j] in Indices G1};
  then p in Values G1 by MATRIX_0:39;
  then p in Values G2 by A1;
  then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
  then consider i,j such that
A10: p = G2*(i,j) and
A11: [i,j] in Indices G2;
A12: 1 <= i by A11,MATRIX_0:32;
A13: i <= len G2 by A11,MATRIX_0:32;
  1 <= j & j <= width G2 by A11,MATRIX_0:32;
  then
A14: G2*(i,j)`1 = G2*(i,1)`1 by A12,A13,GOBOARD5:2
    .= G2*(i,j2)`1 by A7,A12,A13,GOBOARD5:2;
  i1 < i1+1 by NAT_1:13;
  then
A15: G2*(i2,j2)`1 < G2*(i,j2)`1 by A2,A4,A8,A9,A10,A14,GOBOARD5:3;
A16: now
    assume i <= i2;
    then i = i2 or i < i2 by XXREAL_0:1;
    hence contradiction by A6,A7,A12,A15,GOBOARD5:3;
  end;
  assume
A17: p`1 < G2*(i2+1,j2)`1;
A18: 1 <= i2+1 by A5,NAT_1:13;
  now
    assume i2+1 <= i;
    then i2+1 = i or i2+1 < i by XXREAL_0:1;
    hence contradiction by A7,A17,A10,A13,A14,A18,GOBOARD5:3;
  end;
  hence contradiction by A16,NAT_1:13;
end;

theorem Th7:
  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 and
A3: i1 <= len G1 & 1 <= j1 & j1 <= width G1 and
A4: 1 < i2 and
A5: i2 <= len G2 and
A6: 1 <= j2 & j2 <= width G2 and
A7: G1*(i1,j1) = G2*(i2,j2);
  set p = G1*(i1-'1,j1);
A8: p in {G2*(i,j): [i,j] in Indices G2} by A1,MATRIX_0:39;
  1 <= i2-'1 by A4,NAT_D:49;
  then i2-'1 < i2 by NAT_D:51;
  then
A9: i2-'1 < len G2 by A5,XXREAL_0:2;
  consider i,j such that
A10: p = G2*(i,j) and
A11: [i,j] in Indices G2 by A8;
A12: 1 <= i by A11,MATRIX_0:32;
A13: i <= len G2 by A11,MATRIX_0:32;
  1 <= j & j <= width G2 by A11,MATRIX_0:32;
  then
A14: G2*(i,j)`1 = G2*(i,1)`1 by A12,A13,GOBOARD5:2
    .= G2*(i,j2)`1 by A6,A12,A13,GOBOARD5:2;
A15: 1 <= i1-'1 by A2,NAT_D:49;
  then i1-'1 < i1 by NAT_D:51;
  then
A16: G2*(i,j2)`1 < G2*(i2,j2)`1 by A3,A7,A15,A10,A14,GOBOARD5:3;
A17: now
    assume i2 <= i;
    then i = i2 or i2 < i by XXREAL_0:1;
    hence contradiction by A4,A6,A13,A16,GOBOARD5:3;
  end;
  assume
A18: G2*(i2-'1,j2)`1 < p`1;
  now
    assume i <= i2-'1;
    then i2-'1 = i or i < i2-'1 by XXREAL_0:1;
    hence contradiction by A6,A18,A10,A12,A14,A9,GOBOARD5:3;
  end;
  hence contradiction by A17,NAT_D:49;
end;

theorem Th8:
  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 & 1 <= j1 and
A3: j1 < width G1 and
A4: 1 <= i2 & i2 <= len G2 and
A5: 1 <= j2 and
A6: j2 < width G2 and
A7: G1*(i1,j1) = G2*(i2,j2);
  set p = G1*(i1,j1+1);
  p in {G2*(i,j): [i,j] in Indices G2} by A1,MATRIX_0:39;
  then consider i,j such that
A8: p = G2*(i,j) and
A9: [i,j] in Indices G2;
A10: 1 <= j by A9,MATRIX_0:32;
A11: j <= width G2 by A9,MATRIX_0:32;
  1 <= i & i <= len G2 by A9,MATRIX_0:32;
  then
A12: G2*(i,j)`2 = G2*(1,j)`2 by A10,A11,GOBOARD5:1
    .= G2*(i2,j)`2 by A4,A10,A11,GOBOARD5:1;
  j1 < j1+1 & j1+1 <= width G1 by A3,NAT_1:13;
  then
A13: G2*(i2,j2)`2 < G2*(i2,j)`2 by A2,A7,A8,A12,GOBOARD5:4;
A14: now
    assume j <= j2;
    then j = j2 or j < j2 by XXREAL_0:1;
    hence contradiction by A4,A6,A10,A13,GOBOARD5:4;
  end;
  assume
A15: p`2 < G2*(i2,j2+1)`2;
A16: 1 <= j2+1 by A5,NAT_1:13;
  now
    assume j2+1 <= j;
    then j2+1 = j or j2+1 < j by XXREAL_0:1;
    hence contradiction by A4,A15,A8,A11,A12,A16,GOBOARD5:4;
  end;
  hence contradiction by A14,NAT_1:13;
end;

theorem Th9:
  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 and
A4: j1 <= width G1 and
A5: 1 <= i2 & i2 <= len G2 and
A6: 1 < j2 and
A7: j2 <= width G2 and
A8: G1*(i1,j1) = G2*(i2,j2);
  set p = G1*(i1,j1-'1);
A9: 1 <= j1-'1 by A3,NAT_D:49;
  then
A10: j1-'1 < j1 by NAT_D:51;
  then j1-'1 < width G1 by A4,XXREAL_0:2;
  then [i1,j1-'1] in Indices G1 by A2,A9,MATRIX_0:30;
  then p in {G1*(i,j): [i,j] in Indices G1};
  then p in Values G1 by MATRIX_0:39;
  then p in Values G2 by A1;
  then p in {G2*(i,j): [i,j] in Indices G2} by MATRIX_0:39;
  then consider i,j such that
A11: p = G2*(i,j) and
A12: [i,j] in Indices G2;
A13: 1 <= j by A12,MATRIX_0:32;
A14: j <= width G2 by A12,MATRIX_0:32;
  1 <= i & i <= len G2 by A12,MATRIX_0:32;
  then
A15: G2*(i,j)`2 = G2*(1,j)`2 by A13,A14,GOBOARD5:1
    .= G2*(i2,j)`2 by A5,A13,A14,GOBOARD5:1;
  then
A16: G2*(i2,j)`2 < G2*(i2,j2)`2 by A2,A4,A8,A9,A10,A11,GOBOARD5:4;
A17: now
    assume j2 <= j;
    then j = j2 or j2 < j by XXREAL_0:1;
    hence contradiction by A5,A6,A14,A16,GOBOARD5:4;
  end;
  1 <= j2-'1 by A6,NAT_D:49;
  then j2-'1 < j2 by NAT_D:51;
  then
A18: j2-'1 < width G2 by A7,XXREAL_0:2;
  assume
A19: G2*(i2,j2-'1)`2 < p`2;
  now
    assume j <= j2-'1;
    then j2-'1 = j or j < j2-'1 by XXREAL_0:1;
    hence contradiction by A5,A19,A11,A13,A15,A18,GOBOARD5:4;
  end;
  hence contradiction by A17,NAT_D:49;
end;

theorem Th10:
  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);
A5: 1 <= i1 by A2,MATRIX_0:32;
A6: j1 <= width G1 by A2,MATRIX_0:32;
  let p be object such that
A7: p in cell(G2,i2,j2);
A8: 1 <= i2 by A3,MATRIX_0:32;
A9: j2 <= width G2 by A3,MATRIX_0:32;
A10: 1 <= j2 by A3,MATRIX_0:32;
A11: i2 <= len G2 by A3,MATRIX_0:32;
  then
A12: G2*(i2,j2)`1 = G2*(i2,1)`1 & G2*(i2,j2)`2 = G2*(1,j2)`2 by A8,A10,A9,
GOBOARD5:1,2;
A13: 1 <= j1 by A2,MATRIX_0:32;
A14: i1 <= len G1 by A2,MATRIX_0:32;
  then
A15: G1*(i1,j1)`1 = G1*(i1,1)`1 & G1*(i1,j1)`2 = G1*(1,j1)`2 by A5,A13,A6,
GOBOARD5:1,2;
  per cases by A11,A9,XXREAL_0:1;
  suppose
A16: i2 = len G2 & j2 = width G2;
    then
A17: p in { |[r,s]| : G2*(i2,j2)`1 <= r & G2*(i2,j2)`2 <= s } by A7,A12,
GOBRD11:28;
    i1 = len G1 & j1 = width G1 by A1,A2,A4,A8,A10,A16,Th3,Th5;
    hence thesis by A4,A15,A17,GOBRD11:28;
  end;
  suppose
A18: i2 = len G2 & j2 < width G2;
    then p in { |[r,s]| : G2*(i2,j2)`1 <= r & G2*(i2,j2)`2 <= s & s <= G2*(1,
    j2+1)`2 } by A7,A10,A12,GOBRD11:29;
    then consider r9,s9 such that
A19: p = |[r9,s9]| & G2*(i2,j2)`1 <= r9 & G2*(i2,j2)`2 <= s9 and
A20: s9 <= G2*(1,j2+1)`2;
A21: i1 = len G1 by A1,A2,A4,A10,A18,Th3;
    now
      per cases by A6,XXREAL_0:1;
      suppose
A22:    j1 = width G1;
        p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s} by A4,A19;
        hence thesis by A15,A21,A22,GOBRD11:28;
      end;
      suppose
A23:    j1 < width G1;
        1 <= j2+1 & j2+1 <= width G2 by A18,NAT_1:12,13;
        then
A24:    G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A8,A11,GOBOARD5:1;
        1 <= j1+1 & j1+1 <= width G1 by A23,NAT_1:12,13;
        then
        G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A5,A14,
GOBOARD5:1,MATRIX_0:41;
        then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A5,A14,A13,A8,A10,A18,A23
,A24,Th8;
        then s9 <= G1*(1,j1+1)`2 by A20,XXREAL_0:2;
        then
        p in {|[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s & s <= G1*(
        1,j1+1)`2} by A4,A19;
        hence thesis by A13,A15,A21,A23,GOBRD11:29;
      end;
    end;
    hence thesis;
  end;
  suppose
A25: i2 < len G2 & j2 = width G2;
    then p in {|[r,s]|: G2*(i2,j2)`1 <= r & r <= G2*(i2+1,1)`1 & G2*(i2,j2)`2
    <= s} by A7,A8,A12,GOBRD11:31;
    then consider r9,s9 such that
A26: p = |[r9,s9]| & G2*(i2,j2)`1 <= r9 and
A27: r9 <= G2*(i2+1,1)`1 and
A28: G2*(i2,j2)`2 <= s9;
A29: j1 = width G1 by A1,A2,A4,A8,A25,Th5;
    now
      per cases by A14,XXREAL_0:1;
      suppose
A30:    i1 = len G1;
        p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s} by A4,A26,A28;
        hence thesis by A15,A29,A30,GOBRD11:28;
      end;
      suppose
A31:    i1 < len G1;
        1 <= i2+1 & i2+1 <= len G2 by A25,NAT_1:12,13;
        then
A32:    G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A10,A9,GOBOARD5:2;
        1 <= i1+1 & i1+1 <= len G1 by A31,NAT_1:12,13;
        then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A6,GOBOARD5:2;
        then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A6,A8,A10,A25,A31
,A32,Th6;
        then r9 <= G1*(i1+1,1)`1 by A27,XXREAL_0:2;
        then
        p in {|[r,s]|: G1*(i1,j1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*(i1,j1
        )`2 <= s} by A4,A26,A28;
        hence thesis by A5,A15,A29,A31,GOBRD11:31;
      end;
    end;
    hence thesis;
  end;
  suppose
A33: i2 < len G2 & j2 < width G2;
    then 1 <= j2+1 & j2+1 <= width G2 by NAT_1:12,13;
    then
A34: G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A8,A11,GOBOARD5:1;
    1 <= i2+1 & i2+1 <= len G2 by A33,NAT_1:12,13;
    then G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A10,A9,GOBOARD5:2;
    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 A7,A8,A10,A12,A33,A34,GOBRD11:32;
    then consider r9,s9 such that
A35: p = |[r9,s9]| & G2*(i2,j2)`1 <= r9 and
A36: r9 <= G2*(i2+1,j2)`1 and
A37: G2*(i2,j2)`2 <= s9 and
A38: s9 <= G2*(i2,j2+1)`2;
    now
      per cases by A14,A6,XXREAL_0:1;
      suppose
A39:    i1 = len G1 & j1 = width G1;
        p in { |[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s } by A4,A35,A37;
        hence thesis by A15,A39,GOBRD11:28;
      end;
      suppose
A40:    i1 = len G1 & j1 < width G1;
        then 1 <= j1+1 & j1+1 <= width G1 by NAT_1:12,13;
        then
        G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A5,A14,
GOBOARD5:1,MATRIX_0:41;
        then G2*(i2,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A5,A13,A8,A10,A33,A40
,Th8;
        then s9 <= G1*(1,j1+1)`2 by A38,XXREAL_0:2;
        then p in {|[r,s]| : G1*(i1,j1)`1 <= r & G1*(i1,j1)`2 <= s & s <= G1*
        (1,j1+1)`2} by A4,A35,A37;
        hence thesis by A13,A15,A40,GOBRD11:29;
      end;
      suppose
A41:    i1 < len G1 & j1 = width G1;
        then 1 <= i1+1 & i1+1 <= len G1 by NAT_1:12,13;
        then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A6,GOBOARD5:2;
        then G2*(i2+1,j2)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A10,A33,A41
,Th6;
        then r9 <= G1*(i1+1,1)`1 by A36,XXREAL_0:2;
        then
        p in {|[r,s]|: G1*(i1,j1)`1 <= r & r <= G1*(i1+1,1)`1 & G1*(i1,j1
        )`2 <= s} by A4,A35,A37;
        hence thesis by A5,A15,A41,GOBRD11:31;
      end;
      suppose
A42:    i1 < len G1 & j1 < width G1;
        then 1 <= i1+1 & i1+1 <= len G1 by NAT_1:12,13;
        then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A6,GOBOARD5:2;
        then G2*(i2+1,j2)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A10,A33,A42
,Th6;
        then
A43:    r9 <= G1*(i1+1,1)`1 by A36,XXREAL_0:2;
        1 <= j1+1 & j1+1 <= width G1 by A42,NAT_1:12,13;
        then
        G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A5,A14,
GOBOARD5:1,MATRIX_0:41;
        then G2*(i2,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A5,A13,A8,A10,A33,A42
,Th8;
        then s9 <= G1*(1,j1+1)`2 by A38,XXREAL_0:2;
        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,A15,A35,A37,A43;
        hence thesis by A5,A13,A42,GOBRD11:32;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th11:
  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);
A5: i2 <= len G2 by A3,MATRIX_0:32;
A6: j1 <= width G1 by A2,MATRIX_0:32;
A7: 1 <= j1 by A2,MATRIX_0:32;
A8: j2 <= width G2 by A3,MATRIX_0:32;
A9: 1 <= j2 by A3,MATRIX_0:32;
A10: 1 <= i2 by A3,MATRIX_0:32;
  then
A11: G2*(i2,j2)`1 = G2*(i2,1)`1 by A5,A9,A8,GOBOARD5:2;
A12: G2*(i2,j2)`2 = G2*(1,j2)`2 by A10,A5,A9,A8,GOBOARD5:1;
  let p be object such that
A13: p in cell(G2,i2-'1,j2);
A14: 1 <= i1 by A2,MATRIX_0:32;
A15: i1 <= len G1 by A2,MATRIX_0:32;
  per cases by A14,A10,XXREAL_0:1;
  suppose
A16: i1 = 1 & i2 = 1;
    then
A17: i1-'1 = 0 by XREAL_1:232;
A18: i2-'1 = 0 by A16,XREAL_1:232;
    now
      per cases by A8,XXREAL_0:1;
      suppose
A19:    j2 = width G2;
        then
A20:    j1 = width G1 by A1,A2,A4,A10,A5,Th5;
        p in { |[r,s]| : r <= G2*(1,1)`1 & G2*(1,width G2)`2 <= s } by A13,A18
,A19,GOBRD11:25;
        then consider r9,s9 such that
A21:    p = |[r9,s9]| and
A22:    r9 <= G2*(1,1)`1 and
A23:    G2*(1,width G2)`2 <= s9;
        G2*(1,1)`1 = G2*(i1,j2)`1 by A5,A9,A8,A16,GOBOARD5:2;
        then r9 <= G1*(1,1)`1 by A4,A15,A7,A6,A16,A22,GOBOARD5:2;
        then
        p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s } by A4,A16
,A19,A21,A23,A20;
        hence thesis by A17,A20,GOBRD11:25;
      end;
      suppose
A24:    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 A13,A9,A18,GOBRD11:26;
        then consider r9,s9 such that
A25:    p = |[r9,s9]| and
A26:    r9 <= G2*(1,1)`1 and
A27:    G2*(1,j2)`2 <= s9 and
A28:    s9 <= G2*(1,j2+1)`2;
        G2*(1,1)`1 = G2*(i1,j2)`1 by A5,A9,A8,A16,GOBOARD5:2;
        then
A29:    r9 <= G1*(1,1)`1 by A4,A15,A7,A6,A16,A26,GOBOARD5:2;
        now
          per cases by A6,XXREAL_0:1;
          suppose
A30:        j1 = width G1;
            then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
            by A4,A16,A25,A27,A29;
            hence thesis by A17,A30,GOBRD11:25;
          end;
          suppose
A31:        j1 < width G1;
            then 1 <= j1 + 1 & j1 + 1 <= width G1 by NAT_1:11,13;
            then G1*(i1,j1+1) in Values G1 by A14,A15,MATRIX_0:41;
            then
            G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A15,A7,A5,A9,A16,A24,A31
,Th8;
            then s9 <= G1*(1,j1+1)`2 by A28,XXREAL_0:2;
            then
            p in {|[r,s]|: r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s & s <= G1*(
            1,j1+1)`2} by A4,A16,A25,A27,A29;
            hence thesis by A7,A17,A31,GOBRD11:26;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose that
A32: i1 = 1 and
A33: 1 < i2;
A34: i1-'1 = 0 by A32,XREAL_1:232;
A35: 1 <= i2-'1 by A33,NAT_D:49;
    then i2-'1 < i2 by NAT_D:51;
    then
A36: i2-'1 < len G2 by A5,XXREAL_0:2;
A37: i2-'1+1 = i2 by A33,XREAL_1:235;
    now
      per cases by A8,XXREAL_0:1;
      suppose
A38:    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 A13,A35,A36,A37,GOBRD11:31;
        then consider r9,s9 such that
A39:    p = |[r9,s9]| and
        G2*(i2-'1,1)`1 <= r9 and
A40:    r9 <= G2*(i2,1)`1 & G2*(1,j2)`2 <= s9;
        r9 <= G1*(1,1)`1 & G1*(1,j1)`2 <= s9 by A4,A15,A7,A6,A11,A12,A32,A40,
GOBOARD5:2;
        then
A41:    p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s } by A39;
        j1 = width G1 by A1,A2,A4,A10,A5,A38,Th5;
        hence thesis by A34,A41,GOBRD11:25;
      end;
      suppose
A42:    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 A13,A9,A35,A36,A37,GOBRD11:32;
        then consider r9,s9 such that
A43:    p = |[r9,s9]| and
        G2*(i2-'1,1)`1 <= r9 and
A44:    r9 <= G2*(i2,1)`1 & G2*(1,j2)`2 <= s9 and
A45:    s9 <= G2*(1,j2+1)`2;
A46:    r9 <= G1*(1,1)`1 & G1*(1,j1)`2 <= s9 by A4,A15,A7,A6,A11,A12,A32,A44,
GOBOARD5:2;
        now
          per cases by A6,XXREAL_0:1;
          suppose
A47:        j1 = width G1;
            then p in { |[r,s]| : r <= G1*(1,1)`1 & G1*(1,width G1)`2 <= s }
            by A43,A46;
            hence thesis by A34,A47,GOBRD11:25;
          end;
          suppose
A48:        j1 < width G1;
            1 <= j2+1 & j2+1 <= width G2 by A42,NAT_1:12,13;
            then
A49:        G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A10,A5,GOBOARD5:1;
            1 <= j1+1 & j1+1 <= width G1 by A48,NAT_1:12,13;
            then
            G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2 by A14
,A15,GOBOARD5:1,MATRIX_0:41;
            then
            G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A14,A15,A7,A10,A5,A9,A42
,A48,A49,Th8;
            then s9 <= G1*(1,j1+1)`2 by A45,XXREAL_0:2;
            then
            p in {|[r,s]|: r <= G1*(1,1)`1 & G1*(1,j1)`2 <= s & s <= G1*(
            1,j1+1)`2} by A43,A46;
            hence thesis by A7,A34,A48,GOBRD11:26;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose
    1 < i1 & i2 = 1;
    hence thesis by A1,A2,A4,A9,A8,Th2;
  end;
  suppose
A50: 1 < i1 & 1 < i2;
    then
A51: 1 <= i2-'1 by NAT_D:49;
    then
A52: i2-'1+1 = i2 by NAT_D:43;
    i2-'1 < i2 by A51,NAT_D:51;
    then
A53: i2-'1 < len G2 by A5,XXREAL_0:2;
    then
A54: G2*(i2-'1,1)`1 = G2*(i2-'1,j2)`1 by A9,A8,A51,GOBOARD5:2;
A55: 1 <= i1-'1 by A50,NAT_D:49;
    then
A56: i1-'1+1 = i1 by NAT_D:43;
    i1-'1 < i1 by A55,NAT_D:51;
    then
A57: i1-'1 < len G1 by A15,XXREAL_0:2;
    then G1*(i1-'1,j1) in Values G1 & G1*(i1-'1,1)`1 = G1*(i1-'1,j1)`1 by A7,A6
,A55,GOBOARD5:2,MATRIX_0:41;
    then
A58: G1*(i1-'1,1)`1 <= G2*(i2-'1,1)`1 by A1,A4,A15,A7,A6,A5,A9,A8,A50,A54,Th7;
    now
      per cases by A8,XXREAL_0:1;
      suppose
A59:    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 A13,A51,A53,A52,GOBRD11:31;
        then consider r9,s9 such that
A60:    p = |[r9,s9]| and
A61:    G2*(i2-'1,1)`1 <= r9 & r9 <= G2*(i2,1)`1 and
A62:    G2*(1,j2)`2 <= s9;
A63:    G1*(1,j1)`2 <= s9 by A4,A14,A15,A7,A6,A12,A62,GOBOARD5:1;
        G1*(i1-'1,1)`1 <= r9 & r9 <= G1*(i1,1)`1 by A4,A14,A15,A7,A6,A11,A58
,A61,GOBOARD5:2,XXREAL_0:2;
        then
A64:    p in { |[r,s]|: G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 & G1*(1,
        j1)`2 <= s} by A60,A63;
        j1 = width G1 by A1,A2,A4,A10,A5,A59,Th5;
        hence thesis by A55,A57,A56,A64,GOBRD11:31;
      end;
      suppose
A65:    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 A13,A9,A51,A53,A52,GOBRD11:32;
        then consider r9,s9 such that
A66:    p = |[r9,s9]| and
A67:    G2*(i2-'1,1)`1 <= r9 & r9 <= G2*(i2,1)`1 and
A68:    G2*(1,j2)`2 <= s9 and
A69:    s9 <= G2*(1,j2+1)`2;
A70:    G1*(1,j1)`2 <= s9 by A4,A14,A15,A7,A6,A12,A68,GOBOARD5:1;
A71:    G1*(i1-'1,1)`1 <= r9 & r9 <= G1*(i1,1)`1 by A4,A14,A15,A7,A6,A11,A58
,A67,GOBOARD5:2,XXREAL_0:2;
          per cases by A6,XXREAL_0:1;
          suppose
A72:        j1 = width G1;
            p in { |[r,s]|: G1*(i1-'1,1)`1 <= r & r <= G1*(i1,1)`1 & G1*
            (1,j1)`2 <= s } by A66,A71,A70;
            hence thesis by A55,A57,A56,A72,GOBRD11:31;
          end;
          suppose
A73:        j1 < width G1;
            1 <= j2+1 & j2+1 <= width G2 by A65,NAT_1:12,13;
            then
A74:        G2*(i2,j2+1)`2 = G2*(1,j2+1)`2 by A10,A5,GOBOARD5:1;
            1 <= j1+1 & j1+1 <= width G1 by A73,NAT_1:12,13;
            then G1*(i1,j1+1) in Values G1 & G1*(i1,j1+1)`2 = G1*(1,j1+1)`2
            by A14,A15,GOBOARD5:1,MATRIX_0:41;
            then G2*(1,j2+1)`2 <= G1*(1,j1+1)`2 by A1,A4,A14,A15,A7,A10,A5,A9
,A65,A73,A74,Th8;
            then s9 <= G1*(1,j1+1)`2 by A69,XXREAL_0:2;
            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 A66,A71,A70;
            hence thesis by A7,A55,A57,A56,A73,GOBRD11:32;
          end;
      end;
    end;
    hence thesis;
  end;
end;

theorem Th12:
  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);
A5: 1 <= i1 by A2,MATRIX_0:32;
A6: 1 <= j2 by A3,MATRIX_0:32;
A7: 1 <= i2 by A3,MATRIX_0:32;
A8: j1 <= width G1 by A2,MATRIX_0:32;
A9: j2 <= width G2 by A3,MATRIX_0:32;
A10: i2 <= len G2 by A3,MATRIX_0:32;
  then
A11: G2*(i2,j2)`1 = G2*(i2,1)`1 by A7,A6,A9,GOBOARD5:2;
A12: i1 <= len G1 by A2,MATRIX_0:32;
A13: 1 <= j1 by A2,MATRIX_0:32;
then A14: G1*(i1,j1)`2 = G1*(1,j1)`2 by A5,A12,A8,GOBOARD5:1;
  let p be object such that
A15: p in cell(G2,i2,j2-'1);
A16: G2*(i2,j2)`2 = G2*(1,j2)`2 by A7,A10,A6,A9,GOBOARD5:1;
  per cases by A13,A6,XXREAL_0:1;
  suppose
A17: j1 = 1 & j2 = 1;
    then
A18: j1-'1 = 0 by XREAL_1:232;
A19: j2-'1 = 0 by A17,XREAL_1:232;
    now
      per cases by A10,XXREAL_0:1;
      suppose
A20:    i2 = len G2;
        then p in { |[r,s]| : G2*(len G2,1)`1 <= r & s <= G2*(1,1)`2 } by A15
,A19,GOBRD11:27;
        then consider r9,s9 such that
A21:    p = |[r9,s9]| & G2*(len G2,1)`1 <= r9 and
A22:    s9 <= G2*(1,1)`2;
A23:    i1 = len G1 by A1,A2,A4,A6,A9,A20,Th3;
        G2*(1,1)`2 = G2*(i2,j2)`2 by A7,A10,A9,A17,GOBOARD5:1;
        then s9 <= G1*(1,1)`2 by A4,A5,A12,A8,A17,A22,GOBOARD5:1;
        then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 } by A4
,A17,A20,A21,A23;
        hence thesis by A18,A23,GOBRD11:27;
      end;
      suppose
A24:    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 A15,A7,A19,GOBRD11:30;
        then consider r9,s9 such that
A25:    p = |[r9,s9]| & G2*(i2,1)`1 <= r9 and
A26:    r9 <= G2*(i2+1,1)`1 and
A27:    s9 <= G2*(1,1)`2;
        G2*(1,1)`2 = G2*(i2,j1)`2 by A7,A10,A9,A17,GOBOARD5:1;
        then
A28:    s9 <= G1*(1,1)`2 by A4,A5,A12,A8,A17,A27,GOBOARD5:1;
        now
          per cases by A12,XXREAL_0:1;
          suppose
A29:        i1 = len G1;
            then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 } by
A4,A17,A25,A28;
            hence thesis by A18,A29,GOBRD11:27;
          end;
          suppose
A30:        i1 < len G1;
            then
            G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A8,A7,A9,A17,A24,Th6;
            then r9 <= G1*(i1+1,1)`1 by A26,XXREAL_0:2;
            then p in {|[r,s]|: G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & s <=
            G1*(1,1)`2} by A4,A17,A25,A28;
            hence thesis by A5,A18,A30,GOBRD11:30;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose that
A31: j1 = 1 and
A32: 1 < j2;
A33: j1-'1 = 0 by A31,XREAL_1:232;
A34: 1 <= j2-'1 by A32,NAT_D:49;
    then j2-'1 < j2 by NAT_D:51;
    then
A35: j2-'1 < width G2 by A9,XXREAL_0:2;
A36: j2-'1+1 = j2 by A32,XREAL_1:235;
    now
      per cases by A10,XXREAL_0:1;
      suppose
A37:    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 A15,A34,A35,A36,GOBRD11:29;
        then
        ex r9,s9 st p = |[r9,s9]| & G2*(i2,1)`1 <= r9 & G2*(1,j2-'1)`2 <=
        s9 & s9 <= G2*(1,j2)`2;
        then
A38:    p in { |[r,s]| : G1*(i1,1)`1 <= r & s <= G1*(1,1)`2 } by A4,A14,A11,A16
,A31;
        i1 = len G1 by A1,A2,A4,A6,A9,A37,Th3;
        hence thesis by A33,A38,GOBRD11:27;
      end;
      suppose
A39:    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 A15,A7,A34,A35,A36,GOBRD11:32;
        then consider r9,s9 such that
A40:    p = |[r9,s9]| and
A41:    G2*(i2,1)`1 <= r9 and
A42:    r9 <= G2*(i2+1,1)`1 and
        G2*(1,j2-'1)`2 <= s9 and
A43:    s9 <= G2*(1,j2)`2;
A44:    s9 <= G1*(1,1)`2 & G1*(i1,1)`1 <= r9 by A4,A7,A10,A6,A9,A14,A31,A41,A43
,GOBOARD5:1,2;
        now
          per cases by A12,XXREAL_0:1;
          suppose
A45:        i1 = len G1;
            then p in { |[r,s]| : G1*(len G1,1)`1 <= r & s <= G1*(1,1)`2 } by
A40,A44;
            hence thesis by A33,A45,GOBRD11:27;
          end;
          suppose
A46:        i1 < len G1;
            1 <= i2+1 & i2+1 <= len G2 by A39,NAT_1:12,13;
            then
A47:        G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A6,A9,GOBOARD5:2;
            1 <= i1+1 & i1+1 <= len G1 by A46,NAT_1:12,13;
            then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A8,GOBOARD5:2;
            then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A7,A6,A9,A39
,A46,A47,Th6;
            then r9 <= G1*(i1+1,1)`1 by A42,XXREAL_0:2;
            then p in {|[r,s]|: G1*(i1,1)`1 <= r & r <= G1*(i1+1,1)`1 & s <=
            G1*(1,1)`2} by A40,A44;
            hence thesis by A5,A33,A46,GOBRD11:30;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose
    1 < j1 & j2 = 1;
    hence thesis by A1,A2,A4,A7,A10,Th4;
  end;
  suppose
A48: 1 < j1 & 1 < j2;
    then
A49: 1 <= j2-'1 by NAT_D:49;
    then
A50: j2-'1+1 = j2 by NAT_D:43;
    j2-'1 < j2 by A49,NAT_D:51;
    then
A51: j2-'1 < width G2 by A9,XXREAL_0:2;
    then
A52: G2*(1,j2-'1)`2 = G2*(i2,j2-'1)`2 by A7,A10,A49,GOBOARD5:1;
A53: 1 <= j1-'1 by A48,NAT_D:49;
    then
A54: j1-'1+1 = j1 by NAT_D:43;
    j1-'1 < j1 by A53,NAT_D:51;
    then
A55: j1-'1 < width G1 by A8,XXREAL_0:2;
    then G1*(1,j1-'1)`2 = G1*(i1,j1-'1)`2 by A5,A12,A53,GOBOARD5:1;
    then
A56: G1*(1,j1-'1)`2 <= G2*(1,j2-'1)`2 by A1,A4,A5,A12,A8,A7,A10,A9,A48,A52,Th9;
    now
      per cases by A10,XXREAL_0:1;
      suppose
A57:    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 A15,A49,A51,A50,GOBRD11:29;
        then consider r9,s9 such that
A58:    p = |[r9,s9]| and
A59:    G2*(i2,1)`1 <= r9 and
A60:    G2*(1,j2-'1)`2 <= s9 & s9 <= G2*(1,j2)`2;
A61:    G1*(i1,1)`1 <= r9 by A4,A5,A12,A13,A8,A11,A59,GOBOARD5:2;
        G1*(1,j1-'1)`2 <= s9 & s9 <= G1*(1,j1)`2 by A4,A5,A12,A13,A8,A16,A56
,A60,GOBOARD5:1,XXREAL_0:2;
        then
A62:    p in {|[r,s]|: G1*(i1,1)`1 <= r & G1*(1,j1-'1)`2 <= s & s <= G1*(
        1,j1)`2} by A58,A61;
        i1 = len G1 by A1,A2,A4,A6,A9,A57,Th3;
        hence thesis by A53,A55,A54,A62,GOBRD11:29;
      end;
      suppose
A63:    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 A15,A7,A49,A51,A50,GOBRD11:32;
        then consider r9,s9 such that
A64:    p = |[r9,s9]| and
A65:    G2*(i2,1)`1 <= r9 and
A66:    r9 <= G2*(i2+1,1)`1 and
A67:    G2*(1,j2-'1)`2 <= s9 & s9 <= G2*(1,j2)`2;
A68:    G1*(i1,1)`1 <= r9 by A4,A5,A12,A13,A8,A11,A65,GOBOARD5:2;
A69:    G1*(1,j1-'1)`2 <= s9 & s9 <= G1*(1,j1)`2 by A4,A5,A12,A13,A8,A16,A56
,A67,GOBOARD5:1,XXREAL_0:2;
        now
          per cases by A12,XXREAL_0:1;
          suppose
A70:        i1 = len G1;
            p in {|[r,s]|: G1*(i1,1)`1 <= r & G1*(1,j1-'1)`2 <= s & s <=
            G1* (1,j1)`2} by A64,A69,A68;
            hence thesis by A53,A55,A54,A70,GOBRD11:29;
          end;
          suppose
A71:        i1 < len G1;
            1 <= i2+1 & i2+1 <= len G2 by A63,NAT_1:12,13;
            then
A72:        G2*(i2+1,j2)`1 = G2*(i2+1,1)`1 by A6,A9,GOBOARD5:2;
            1 <= i1+1 & i1+1 <= len G1 by A71,NAT_1:12,13;
            then G1*(i1+1,j1)`1 = G1*(i1+1,1)`1 by A13,A8,GOBOARD5:2;
            then G2*(i2+1,1)`1 <= G1*(i1+1,1)`1 by A1,A4,A5,A13,A8,A7,A6,A9,A63
,A71,A72,Th6;
            then r9 <= G1*(i1+1,1)`1 by A66,XXREAL_0:2;
            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 A64,A69,A68;
            hence thesis by A5,A53,A55,A54,A71,GOBRD11:32;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
end;

Lm1: 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 that
A1: 1 <= i & i <= len GoB f and
A2: 1 <= j & j <= width GoB f;
A3: GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
  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:25;
  then (Incr X_axis f).i in rng Incr X_axis f by FUNCT_1:def 3;
  then (Incr X_axis f).i in rng X_axis f by SEQ_4:def 21;
  then consider k being Nat such that
A4: k in dom X_axis f and
A5: (X_axis f).k = (Incr X_axis f).i by FINSEQ_2:10;
  [i,j] in Indices GoB f by A1,A2,MATRIX_0:30;
  then
A6: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A3,GOBOARD2:def 1;
  reconsider k as Nat;
  take k;
  len X_axis f = len f by GOBOARD1:def 1;
  hence k in dom f by A4,FINSEQ_3:29;
  thus (f/.k)`1 = Incr(X_axis f).i by A4,A5,GOBOARD1:def 1
    .= (GoB f)*(i,j)`1 by A6,EUCLID:52;
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)`2 = (GoB f)*(i,j)`2
proof
  let f be non empty FinSequence of TOP-REAL 2;
  assume that
A1: 1 <= i & i <= len GoB f and
A2: 1 <= j & j <= width GoB f;
A3: GoB f = GoB (Incr X_axis f,Incr Y_axis f) by GOBOARD2:def 2;
  then len Incr Y_axis f = width GoB f by GOBOARD2:def 1;
  then j in dom Incr Y_axis f by A2,FINSEQ_3:25;
  then (Incr Y_axis f).j in rng Incr Y_axis f by FUNCT_1:def 3;
  then (Incr Y_axis f).j in rng Y_axis f by SEQ_4:def 21;
  then consider k being Nat such that
A4: k in dom Y_axis f and
A5: (Y_axis f).k = (Incr Y_axis f).j by FINSEQ_2:10;
  [i,j] in Indices GoB f by A1,A2,MATRIX_0:30;
  then
A6: (GoB f)*(i,j) = |[Incr(X_axis f).i,Incr(Y_axis f).j]| by A3,GOBOARD2:def 1;
  reconsider k as Nat;
  take k;
  len Y_axis f = len f by GOBOARD1:def 2;
  hence k in dom f by A4,FINSEQ_3:29;
  thus (f/.k)`2 = Incr(Y_axis f).j by A4,A5,GOBOARD1:def 2
    .= (GoB f)*(i,j)`2 by A6,EUCLID:52;
end;

theorem Th13:
  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;
  let p be object;
  set F = GoB f;
  assume p in Values F;
  then p in { F*(i,j): [i,j] in Indices F } by MATRIX_0:39;
  then consider i,j such that
A2: p = F*(i,j) and
A3: [i,j] in Indices F;
  reconsider p as Point of TOP-REAL 2 by A2;
A4: 1 <= j & j <= width F by A3,MATRIX_0:32;
A5: 1 <= i & i <= len F by A3,MATRIX_0:32;
  then consider k1 such that
A6: k1 in dom f and
A7: p`1 = (f/.k1)`1 by A2,A4,Lm1;
  consider k2 such that
A8: k2 in dom f and
A9: p`2 = (f/.k2)`2 by A2,A5,A4,Lm2;
  consider i2,j2 such that
A10: [i2,j2] in Indices G and
A11: f/.k2 = G*(i2,j2) by A1,A8,GOBOARD1:def 9;
A12: 1 <= i2 & i2 <= len G by A10,MATRIX_0:32;
  consider i1,j1 such that
A13: [i1,j1] in Indices G and
A14: f/.k1 = G*(i1,j1) by A1,A6,GOBOARD1:def 9;
A15: 1 <= j1 & j1 <= width G by A13,MATRIX_0:32;
A16: p = |[p`1, p`2]| by EUCLID:53;
A17: 1 <= j2 & j2 <= width G by A10,MATRIX_0:32;
A18: 1 <= i1 & i1 <= len G by A13,MATRIX_0:32;
  then
A19: [i1,j2] in Indices G by A17,MATRIX_0:30;
A20: G*(i1,j2)`2 = G*(1,j2)`2 by A18,A17,GOBOARD5:1
    .= G*(i2,j2)`2 by A12,A17,GOBOARD5:1;
  G*(i1,j2)`1 = G*(i1,1)`1 by A18,A17,GOBOARD5:2
    .= G*(i1,j1)`1 by A18,A15,GOBOARD5:2;
  then p = G*(i1,j2) by A7,A9,A14,A11,A20,A16,EUCLID:53;
  then p in { G*(k,l): [k,l] in Indices G } by A19;
  hence thesis by MATRIX_0:39;
end;

definition
::$CD
  let f, G, k;
  assume 1 <= k & k+1 <= len f & f is_sequence_on G;
  then consider i1,j1,i2,j2 being Nat such that
A1: [i1,j1] in Indices G & f/.k = G*(i1,j1) and
A2: [i2,j2] in Indices G & f/.(k+1) = G*(i2,j2) and
A3: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
  i1 = i2 & j1 = j2+1 by JORDAN8:3;
  func right_cell(f,k,G) -> Subset of TOP-REAL 2 means
  :Def1:
  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 A3;
    suppose
A4:   i1 = i2 & j1+1 = j2;
      take cell(G,i1,j1);
      let i19,j19,i29,j29 be Nat;
      assume that
A5:   [i19,j19] in Indices G and
A6:   [i29,j29] in Indices G and
A7:   f/.k = G*(i19,j19) and
A8:   f/.(k+1) = G*(i29,j29);
      i1 = i19 & j1 = j19 by A1,A5,A7,GOBOARD1:5;
      hence thesis by A2,A4,A6,A8,GOBOARD1:5;
    end;
    suppose
A9:   i1+1 = i2 & j1 = j2;
      take cell(G,i1,j1-'1);
      let i19,j19,i29,j29 be Nat;
      assume that
A10:  [i19,j19] in Indices G and
A11:  [i29,j29] in Indices G and
A12:  f/.k = G*(i19,j19) and
A13:  f/.(k+1) = G*(i29,j29);
      i1 = i19 & j1 = j19 by A1,A10,A12,GOBOARD1:5;
      hence thesis by A2,A9,A11,A13,GOBOARD1:5;
    end;
    suppose
A14:  i1 = i2+1 & j1 = j2;
      take cell(G,i2,j2);
      let i19,j19,i29,j29 be Nat;
      assume
A15:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,A2,GOBOARD1:5;
      hence thesis by A1,A2,A14,A15,GOBOARD1:5;
    end;
    suppose
A16:  i1 = i2 & j1 = j2+1;
      take cell(G,i1-'1,j2);
      let i19,j19,i29,j29 be Nat;
      assume that
A17:  [i19,j19] in Indices G and
A18:  [i29,j29] in Indices G and
A19:  f/.k = G*(i19,j19) and
A20:  f/.(k+1) = G*(i29,j29);
      i1 = i19 & j1 = j19 by A1,A17,A19,GOBOARD1:5;
      hence thesis by A2,A16,A18,A20,GOBOARD1:5;
    end;
  end;
  uniqueness
  proof
    let P1,P2 be Subset of TOP-REAL 2 such that
A21: 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
A22: 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 A3;
    suppose
A23:  i1 = i2 & j1+1 = j2;
A24:  j2 <= j2+1 by NAT_1:11;
A25:  j1 < j2 by A23,XREAL_1:29;
      hence P1 = cell(G,i1,j1) by A1,A2,A21,A24
        .= P2 by A1,A2,A22,A25,A24;
    end;
    suppose
A26:  i1+1 = i2 & j1 = j2;
A27:  i2 <= i2+1 by NAT_1:11;
A28:  i1 < i2 by A26,XREAL_1:29;
      hence P1 = cell(G,i1,j1-'1) by A1,A2,A21,A27
        .= P2 by A1,A2,A22,A28,A27;
    end;
    suppose
A29:  i1 = i2+1 & j1 = j2;
A30:  i1 <= i1+1 by NAT_1:11;
A31:  i2 < i1 by A29,XREAL_1:29;
      hence P1 = cell(G,i2,j2) by A1,A2,A21,A30
        .= P2 by A1,A2,A22,A31,A30;
    end;
    suppose
A32:  i1 = i2 & j1 = j2+1;
A33:  j1 <= j1+1 by NAT_1:11;
A34:  j2 < j1 by A32,XREAL_1:29;
      hence P1 = cell(G,i1-'1,j2) by A1,A2,A21,A33
        .= P2 by A1,A2,A22,A34,A33;
    end;
  end;
  func left_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-'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 A3;
    suppose
A35:  i1 = i2 & j1+1 = j2;
      take cell(G,i1-'1,j1);
      let i19,j19,i29,j29 be Nat;
      assume that
A36:  [i19,j19] in Indices G and
A37:  [i29,j29] in Indices G and
A38:  f/.k = G*(i19,j19) and
A39:  f/.(k+1) = G*(i29,j29);
      i1 = i19 & j1 = j19 by A1,A36,A38,GOBOARD1:5;
      hence thesis by A2,A35,A37,A39,GOBOARD1:5;
    end;
    suppose
A40:  i1+1 = i2 & j1 = j2;
      take cell(G,i1,j1);
      let i19,j19,i29,j29 be Nat;
      assume that
A41:  [i19,j19] in Indices G and
A42:  [i29,j29] in Indices G and
A43:  f/.k = G*(i19,j19) and
A44:  f/.(k+1) = G*(i29,j29);
      i1 = i19 & j1 = j19 by A1,A41,A43,GOBOARD1:5;
      hence thesis by A2,A40,A42,A44,GOBOARD1:5;
    end;
    suppose
A45:  i1 = i2+1 & j1 = j2;
      take cell(G,i2,j2-'1);
      let i19,j19,i29,j29 be Nat;
      assume
A46:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,A2,GOBOARD1:5;
      hence thesis by A1,A2,A45,A46,GOBOARD1:5;
    end;
    suppose
A47:  i1 = i2 & j1 = j2+1;
      take cell(G,i1,j2);
      let i19,j19,i29,j29 be Nat;
      assume that
A48:  [i19,j19] in Indices G and
A49:  [i29,j29] in Indices G and
A50:  f/.k = G*(i19,j19) and
A51:  f/.(k+1) = G*(i29,j29);
      i1 = i19 & j1 = j19 by A1,A48,A50,GOBOARD1:5;
      hence thesis by A2,A47,A49,A51,GOBOARD1:5;
    end;
  end;
  uniqueness
  proof
    let P1,P2 be Subset of TOP-REAL 2 such that
A52: 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
A53: 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 A3;
    suppose
A54:  i1 = i2 & j1+1 = j2;
A55:  j2 <= j2+1 by NAT_1:11;
A56:  j1 < j2 by A54,XREAL_1:29;
      hence P1 = cell(G,i1-'1,j1) by A1,A2,A52,A55
        .= P2 by A1,A2,A53,A56,A55;
    end;
    suppose
A57:  i1+1 = i2 & j1 = j2;
A58:  i2 <= i2+1 by NAT_1:11;
A59:  i1 < i2 by A57,XREAL_1:29;
      hence P1 = cell(G,i1,j1) by A1,A2,A52,A58
        .= P2 by A1,A2,A53,A59,A58;
    end;
    suppose
A60:  i1 = i2+1 & j1 = j2;
A61:  i1 <= i1+1 by NAT_1:11;
A62:  i2 < i1 by A60,XREAL_1:29;
      hence P1 = cell(G,i2,j2-'1) by A1,A2,A52,A61
        .= P2 by A1,A2,A53,A62,A61;
    end;
    suppose
A63:  i1 = i2 & j1 = j2+1;
A64:  j1 <= j1+1 by NAT_1:11;
A65:  j2 < j1 by A63,XREAL_1:29;
      hence P1 = cell(G,i1,j2) by A1,A2,A52,A64
        .= P2 by A1,A2,A53,A65,A64;
    end;
  end;
end;

theorem Th14:
  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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def2;
end;

theorem Th15:
  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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def1;
end;

theorem Th16:
  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
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def2;
end;

theorem Th17:
  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
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def1;
end;

theorem Th18:
  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
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def2;
end;

theorem Th19:
  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
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def1;
end;

theorem Th20:
  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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def2;
end;

theorem Th21:
  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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def1;
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 and
A2: k+1 <= len f and
A3: f is_sequence_on G;
  k+1 >= 1 by NAT_1:11;
  then
A4: k+1 in dom f by A2,FINSEQ_3:25;
  then consider i2,j2 being Nat such that
A5: [i2,j2] in Indices G and
A6: f/.(k+1) = G*(i2,j2) by A3,GOBOARD1:def 9;
A7: 1 <= j2 by A5,MATRIX_0:32;
A8: i2 <= len G by A5,MATRIX_0:32;
A9: 1 <= i2 by A5,MATRIX_0:32;
A10: j2 <= width G by A5,MATRIX_0:32;
  k <= k+1 by NAT_1:11;
  then k <= len f by A2,XXREAL_0:2;
  then
A11: k in dom f by A1,FINSEQ_3:25;
  then consider i1,j1 being Nat such that
A12: [i1,j1] in Indices G and
A13: f/.k = G*(i1,j1) by A3,GOBOARD1:def 9;
A14: 0+1 <= j1 by A12,MATRIX_0:32;
  then j1 > 0;
  then consider j being Nat such that
A15: j+1 = j1 by NAT_1:6;
A16: |.i1-i2.|+|.j1-j2.| = 1 by A3,A11,A12,A13,A4,A5,A6,GOBOARD1:def 9;
A17: now
    per cases by A16,SEQM_3:42;
    case that
A18:  |.i1-i2.| = 1 and
A19:  j1 = j2;
      i1-i2 = 1 or -(i1-i2) = 1 by A18,ABSVALUE:def 1;
      hence i1 = i2+1 or i1+1 = i2;
      thus j1 = j2 by A19;
    end;
    case that
A20:  i1 = i2 and
A21:  |.j1-j2.| = 1;
      j1-j2 = 1 or -(j1-j2) = 1 by A21,ABSVALUE:def 1;
      hence j1 = j2+1 or j1+1 = j2;
      thus i1 = i2 by A20;
    end;
  end;
A22: j1-'1=j by A15,NAT_D:34;
A23: j1 <= width G by A12,MATRIX_0:32;
  then
A24: j < width G by A15,NAT_1:13;
A25: 0+1 <= i1 by A12,MATRIX_0:32;
  then i1 > 0;
  then consider i being Nat such that
A26: i+1 = i1 by NAT_1:6;
A27: i1 <= len G by A12,MATRIX_0:32;
  then
A28: i < len G by A26,NAT_1:13;
A29: i1-'1 = i by A26,NAT_D:34;
  reconsider i,j as Nat;
  per cases by A17;
  suppose
A30: i1 = i2 & j1+1 = j2;
    then
A31: right_cell(f,k,G) = cell(G,i1,j1) by A1,A2,A3,A12,A13,A5,A6,Th15;
    j1 < width G & left_cell(f,k,G) = cell(G,i,j1) by A1,A2,A3,A12,A13,A5,A6
,A10,A29,A30,Th14,NAT_1:13;
    hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i1,j1),G*(i1,j1+1))
    by A14,A26,A28,A31,GOBOARD5:25
      .= LSeg(f,k) by A1,A2,A13,A6,A30,TOPREAL1:def 3;
  end;
  suppose
A32: i1+1 = i2 & j1 = j2;
    then
A33: right_cell(f,k,G) = cell(G,i1,j) by A1,A2,A3,A12,A13,A5,A6,A22,Th17;
    i1 < len G & left_cell(f,k,G) = cell(G,i1,j1) by A1,A2,A3,A12,A13,A5,A6,A8
,A32,Th16,NAT_1:13;
    hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i1,j1),G*(i1+1,j1))
    by A25,A15,A24,A33,GOBOARD5:26
      .= LSeg(f,k) by A1,A2,A13,A6,A32,TOPREAL1:def 3;
  end;
  suppose
A34: i1 = i2+1 & j1 = j2;
    then
A35: right_cell(f,k,G) = cell(G,i2,j1) by A1,A2,A3,A12,A13,A5,A6,Th19;
    i2 < len G & left_cell(f,k,G) = cell(G,i2,j) by A1,A2,A3,A12,A13,A5,A6,A27
,A22,A34,Th18,NAT_1:13;
    hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i2+1,j1),G*(i2,j1))
    by A9,A15,A24,A35,GOBOARD5:26
      .= LSeg(f,k) by A1,A2,A13,A6,A34,TOPREAL1:def 3;
  end;
  suppose
A36: i1 = i2 & j1 = j2+1;
    then
A37: right_cell(f,k,G) = cell(G,i,j2) by A1,A2,A3,A12,A13,A5,A6,A29,Th21;
    j2 < width G & left_cell(f,k,G) = cell(G,i1,j2) by A1,A2,A3,A12,A13,A5,A6
,A23,A36,Th20,NAT_1:13;
    hence left_cell(f,k,G) /\ right_cell(f,k,G) = LSeg(G*(i1,j2+1),G*(i1,j2))
    by A7,A26,A28,A37,GOBOARD5:25
      .= LSeg(f,k) by A1,A2,A13,A6,A36,TOPREAL1:def 3;
  end;
end;

theorem
  1 <= k & k+1 <= len f & f is_sequence_on G implies right_cell(f,k,G)
  is closed
proof
  assume
A1: 1 <= k & k+1 <= len f & f is_sequence_on G;
  then consider i1,j1,i2,j2 being Nat such that
A2: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f/.
( k+1 ) = G*(i2,j2) &( i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1
  & j1 = j2 or i1 = i2 & j1 = j2+1) by JORDAN8:3;
  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,Def1;
  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 and
A2: k+1 <= len f and
A3: f is_sequence_on G and
A4: k+1 <= n;
  per cases;
  suppose
    len f <= n;
    hence thesis by FINSEQ_1:58;
  end;
  suppose
    n < len f;
    then
A5: len(f|n) = n by FINSEQ_1:59;
    then k in dom(f|n) by A1,A4,SEQ_4:134;
    then
A6: (f|n)/.k = f/.k by FINSEQ_4:70;
    k+1 in dom(f|n) by A1,A4,A5,SEQ_4:134;
    then
A7: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
    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);
A8: f|n is_sequence_on G by A3,GOBOARD1:22;
    consider i1,j1,i2,j2 being Nat such that
A9: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f
    /.( k+1) = G*(i2,j2) and
A10: 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,A3,JORDAN8:3;
A11: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A12: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
    now
      per cases by A10;
      suppose
A13:    i1 = i2 & j1+1 = j2;
        hence lf = cell(G,i1-'1,j1) by A1,A2,A3,A9,A11,Def2
          .= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def2;
        thus rf = cell(G,i1,j1) by A1,A2,A3,A9,A11,A13,Def1
          .= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def1;
      end;
      suppose
A14:    i1+1 = i2 & j1 = j2;
        hence lf = cell(G,i1,j1) by A1,A2,A3,A9,A12,Def2
          .= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def2;
        thus rf = cell(G,i1,j1-'1) by A1,A2,A3,A9,A12,A14,Def1
          .= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def1;
      end;
      suppose
A15:    i1 = i2+1 & j1 = j2;
        hence lf = cell(G,i2,j2-'1) by A1,A2,A3,A9,A12,Def2
          .= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def2;
        thus rf = cell(G,i2,j2) by A1,A2,A3,A9,A12,A15,Def1
          .= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def1;
      end;
      suppose
A16:    i1 = i2 & j1 = j2+1;
        hence lf = cell(G,i1,j2) by A1,A2,A3,A9,A11,Def2
          .= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def2;
        thus rf = cell(G,i1-'1,j2) by A1,A2,A3,A9,A11,A16,Def1
          .= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def1;
      end;
    end;
    hence thesis;
  end;
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 and
A2: k+1 <= len g and
A3: n <= len f and
A4: f is_sequence_on G;
A5: len g = len f - n & k+1+n <= (len g)+n by A2,A3,RFINSEQ:def 1,XREAL_1:6;
  k in dom g by A1,A2,SEQ_4:134;
  then
A6: g/.k = f/.(k+n) by FINSEQ_5:27;
  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);
A7: k+1+n = k+n+1 & 1 <= k+n by A1,NAT_1:12;
  k+1 in dom g by A1,A2,SEQ_4:134;
  then
A8: g/.(k+1) = f/.(k+1+n) by FINSEQ_5:27;
A9: g is_sequence_on G by A4,JORDAN8:2;
  then consider i1,j1,i2,j2 being Nat such that
A10: [i1,j1] in Indices G & g/.k = G*(i1,j1) & [i2,j2] in Indices G & g/.
  ( k+1) = G*(i2,j2) and
A11: 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:3;
A12: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A13: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
  now
    per cases by A11;
    suppose
A14:  i1 = i2 & j1+1 = j2;
      hence lf = cell(G,i1-'1,j1) by A4,A10,A12,A6,A8,A5,A7,Def2
        .= lfn by A1,A2,A9,A10,A12,A14,Def2;
      thus rf = cell(G,i1,j1) by A4,A10,A12,A6,A8,A5,A7,A14,Def1
        .= rfn by A1,A2,A9,A10,A12,A14,Def1;
    end;
    suppose
A15:  i1+1 = i2 & j1 = j2;
      hence lf = cell(G,i1,j1) by A4,A10,A13,A6,A8,A5,A7,Def2
        .= lfn by A1,A2,A9,A10,A13,A15,Def2;
      thus rf = cell(G,i1,j1-'1) by A4,A10,A13,A6,A8,A5,A7,A15,Def1
        .= rfn by A1,A2,A9,A10,A13,A15,Def1;
    end;
    suppose
A16:  i1 = i2+1 & j1 = j2;
      hence lf = cell(G,i2,j2-'1) by A4,A10,A13,A6,A8,A5,A7,Def2
        .= lfn by A1,A2,A9,A10,A13,A16,Def2;
      thus rf = cell(G,i2,j2) by A4,A10,A13,A6,A8,A5,A7,A16,Def1
        .= rfn by A1,A2,A9,A10,A13,A16,Def1;
    end;
    suppose
A17:  i1 = i2 & j1 = j2+1;
      hence lf = cell(G,i1,j2) by A4,A10,A12,A6,A8,A5,A7,Def2
        .= lfn by A1,A2,A9,A10,A12,A17,Def2;
      thus rf = cell(G,i1-'1,j2) by A4,A10,A12,A6,A8,A5,A7,A17,Def1
        .= rfn by A1,A2,A9,A10,A12,A17,Def1;
    end;
  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;
  consider i1,j1,i2,j2 such that
A3: [i1,j1] in Indices G and
A4: f/.n = G*(i1,j1) and
A5: [i2,j2] in Indices G and
A6: f/.(n+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:3;
A8: 1 <= j1 by A3,MATRIX_0:32;
A9: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A10: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
A11: j2 <= width G by A5,MATRIX_0:32;
A12: j1 <= width G by A3,MATRIX_0:32;
A13: i2 <= len G by A5,MATRIX_0:32;
A14: 1 <= i2 by A5,MATRIX_0:32;
  then
A15: G*(i2,j1)`2 = G*(1,j1)`2 by A8,A12,A13,GOBOARD5:1;
A16: 1 <= j2 by A5,MATRIX_0:32;
  then
A17: G*(i2,j2)`1 = G*(i2,1)`1 by A14,A13,A11,GOBOARD5:2;
A18: i1 <= len G by A3,MATRIX_0:32;
  set F = GoB f;
A19: Values F c= Values G by A2,Th13;
  f is_sequence_on F by GOBOARD5:def 5;
  then consider m,k,i,j such that
A20: [m,k] in Indices F and
A21: f/.n = F*(m,k) and
A22: [i,j] in Indices F and
A23: 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:3;
A24: 1 <= m by A20,MATRIX_0:32;
A25: 1 <= i1 by A3,MATRIX_0:32;
  then
A26: G*(i1,j1)`1 = G*(i1,1)`1 by A18,A8,A12,GOBOARD5:2;
A27: G*(i1,j1)`2 = G*(1,j1)`2 by A25,A18,A8,A12,GOBOARD5:1;
A28: m <= len F by A20,MATRIX_0:32;
A29: j+1 > j by NAT_1:13;
A30: k+1 > k by NAT_1:13;
A31: k+1 >= 1 by NAT_1:12;
A32: j+1 >= 1 by NAT_1:12;
A33: j <= width F by A22,MATRIX_0:32;
A34: i+1 > i by NAT_1:13;
A35: m+1 > m by NAT_1:13;
A36: i <= len F by A22,MATRIX_0:32;
A37: i+1 >= 1 by NAT_1:12;
A38: m+1 >= 1 by NAT_1:12;
A39: k <= width F by A20,MATRIX_0:32;
A40: 1 <= j by A22,MATRIX_0:32;
  then
A41: F*(m,j)`2 = F*(1,j)`2 by A24,A28,A33,GOBOARD5:1;
A42: 1 <= i by A22,MATRIX_0:32;
  then
A43: F*(i,j)`1 = F*(i,1)`1 by A36,A40,A33,GOBOARD5:2;
A44: F*(i,j)`2 = F*(1,j)`2 by A42,A36,A40,A33,GOBOARD5:1;
A45: 1 <= k by A20,MATRIX_0:32;
  then
A46: F*(i,k)`1 = F*(i,1)`1 by A39,A42,A36,GOBOARD5:2;
  per cases by A7;
  suppose
A47: i1 = i2 & j1+1 = j2;
A48: now
A49:  G*(i2,j2)`2 = G*(1,j2)`2 by A14,A13,A16,A11,GOBOARD5:1;
      assume
A50:  k+1 < j;
      then
A51:  k+1 < width F by A33,XXREAL_0:2;
      then consider l,i9 such that
A52:  l in dom f and
A53:  [i9,k+1] in Indices F and
A54:  f/.l = F*(i9,k+1) by JORDAN5D:8,NAT_1:12;
A55:  F*(m,k+1)`2 = F*(1,k+1)`2 by A24,A28,A31,A51,GOBOARD5:1;
      1 <= i9 & i9 <= len F by A53,MATRIX_0:32;
      then
A56:  F*(i9,k+1)`2 = F*(1,k+1)`2 by A31,A51,GOBOARD5:1;
      consider i19,j19 such that
A57:  [i19,j19] in Indices G and
A58:  f/.l = G*(i19,j19) by A2,A52,GOBOARD1:def 9;
A59:  1 <= j19 by A57,MATRIX_0:32;
A60:  1 <= i19 & i19 <= len G by A57,MATRIX_0:32;
      then
A61:  G*(i19,j1)`2 = G*(1,j1)`2 by A8,A12,GOBOARD5:1;
A62:  now
        assume j1 >= j19;
        then G*(i19,j19)`2 <= G*(i1,j1)`2 by A12,A27,A60,A59,A61,SPRECT_3:12;
        hence contradiction by A21,A24,A28,A45,A4,A30,A51,A54,A56,A55,A58,
GOBOARD5:4;
      end;
A63:  j19 <= width G by A57,MATRIX_0:32;
A64:  G*(i19,j2)`2 = G*(1,j2)`2 by A16,A11,A60,GOBOARD5:1;
      now
        assume j2 <= j19;
        then G*(i2,j2)`2 <= G*(i19,j19)`2 by A16,A60,A63,A49,A64,SPRECT_3:12;
        hence contradiction by A23,A24,A28,A33,A44,A41,A6,A31,A50,A54,A56,A55
,A58,GOBOARD5:4;
      end;
      hence contradiction by A47,A62,NAT_1:13;
    end;
    now
      assume j <= k;
      then
A65:  F*(i,j)`2 <= F*(m,k)`2 by A24,A28,A39,A40,A44,A41,SPRECT_3:12;
      j1 < j2 by A47,NAT_1:13;
      hence contradiction by A21,A23,A4,A6,A8,A14,A13,A11,A27,A15,A65,
GOBOARD5:4;
    end;
    then k+1 <= j by NAT_1:13;
    then k+1 = j by A48,XXREAL_0:1;
    then
A66: right_cell(f,n) = cell(F,m,k) & left_cell(f,n) = cell(F,m-'1,k) by A1,A20
,A21,A22,A23,A30,A29,GOBOARD5:def 6,def 7;
    right_cell(f,n,G) = cell(G,i1,j1) & left_cell(f,n,G) = cell(G,i1-'1,
    j1) by A1,A2,A3,A4,A5,A6,A9,A47,Def1,Def2;
    hence thesis by A19,A20,A21,A3,A4,A66,Th10,Th11;
  end;
  suppose
A67: i1+1 = i2 & j1 = j2;
A68: now
      assume
A69:  m+1 < i;
      then
A70:  m+1 < len F by A36,XXREAL_0:2;
      then consider l,j9 such that
A71:  l in dom f and
A72:  [m+1,j9] in Indices F and
A73:  f/.l = F*(m+1,j9) by JORDAN5D:7,NAT_1:12;
A74:  F*(m+1,k)`1 = F*(m+1,1)`1 by A45,A39,A38,A70,GOBOARD5:2;
      1 <= j9 & j9 <= width F by A72,MATRIX_0:32;
      then
A75:  F*(m+1,j9)`1 = F*(m+1,1)`1 by A38,A70,GOBOARD5:2;
A76:  1 <= m+1 & F*(m+1,j)`1 = F*(m+1,1)`1 by A40,A33,A38,A70,GOBOARD5:2;
A77:  G*(i2,j2)`1 = G*(i2,1)`1 by A14,A13,A16,A11,GOBOARD5:2;
      consider i19,j19 such that
A78:  [i19,j19] in Indices G and
A79:  f/.l = G*(i19,j19) by A2,A71,GOBOARD1:def 9;
A80:  i19 <= len G by A78,MATRIX_0:32;
A81:  1 <= j19 & j19 <= width G by A78,MATRIX_0:32;
A82:  1 <= i19 by A78,MATRIX_0:32;
      then
A83:  G*(i19,j19)`1 = G*(i19,1)`1 by A80,A81,GOBOARD5:2;
A84:  G*(i19,j1)`1 = G*(i19,1)`1 by A8,A12,A82,A80,GOBOARD5:2;
A85:  now
        assume i1 >= i19;
        then G*(i19,j19)`1 <= G*(i1,j1)`1 by A18,A8,A12,A82,A83,A84,SPRECT_3:13
;
        hence contradiction by A21,A24,A45,A39,A4,A35,A70,A73,A75,A74,A79,
GOBOARD5:3;
      end;
A86:  G*(i2,j19)`1 = G*(i2,1)`1 by A14,A13,A81,GOBOARD5:2;
      now
        assume i2 <= i19;
        then G*(i2,j2)`1 <= G*(i19,j19)`1 by A14,A80,A81,A77,A86,SPRECT_3:13;
        hence contradiction by A23,A36,A40,A33,A6,A69,A73,A75,A76,A79,
GOBOARD5:3;
      end;
      hence contradiction by A67,A85,NAT_1:13;
    end;
    now
      assume i <= m;
      then
A87:  F*(i,j)`1 <= F*(m,k)`1 by A28,A45,A39,A42,A43,A46,SPRECT_3:13;
      i1 < i2 by A67,NAT_1:13;
      hence contradiction by A21,A23,A4,A6,A25,A8,A12,A13,A67,A87,GOBOARD5:3;
    end;
    then m+1 <= i by NAT_1:13;
    then m+1 = i by A68,XXREAL_0:1;
    then
A88: right_cell(f,n) = cell(F,m, k-'1) & left_cell(f,n) = cell(F,m,k) by A1,A20
,A21,A22,A23,A35,A34,GOBOARD5:def 6,def 7;
    right_cell(f,n,G) = cell(G,i1,j1-'1) & left_cell(f,n,G) = cell(G,i1,
    j1) by A1,A2,A3,A4,A5,A6,A10,A67,Def1,Def2;
    hence thesis by A19,A20,A21,A3,A4,A88,Th10,Th12;
  end;
  suppose
A89: i1 = i2+1 & j1 = j2;
A90: now
      assume
A91:  m > i+1;
      then
A92:  i+1 < len F by A28,XXREAL_0:2;
      then consider l,j9 such that
A93:  l in dom f and
A94:  [i+1,j9] in Indices F and
A95:  f/.l = F*(i+1,j9) by JORDAN5D:7,NAT_1:12;
A96:  1 <= i+1 & F*(i+1,k)`1 = F*(i+1,1)`1 by A45,A39,A37,A92,GOBOARD5:2;
      1 <= j9 & j9 <= width F by A94,MATRIX_0:32;
      then
A97:  F*(i+1,j9)`1 = F*(i+1,1)`1 by A37,A92,GOBOARD5:2;
A98:  F*(i+1,j)`1 = F*(i+1,1)`1 by A40,A33,A37,A92,GOBOARD5:2;
A99:  G*(i2,j2)`1 = G*(i2,1)`1 by A14,A13,A16,A11,GOBOARD5:2;
      consider i19,j19 such that
A100: [i19,j19] in Indices G and
A101: f/.l = G*(i19,j19) by A2,A93,GOBOARD1:def 9;
A102: 1 <= i19 by A100,MATRIX_0:32;
A103: 1 <= j19 & j19 <= width G by A100,MATRIX_0:32;
A104: i19 <= len G by A100,MATRIX_0:32;
      then
A105: G*(i19,j19)`1 = G*(i19,1)`1 by A102,A103,GOBOARD5:2;
A106: G*(i19,j1)`1 = G*(i19,1)`1 by A8,A12,A102,A104,GOBOARD5:2;
A107: now
        assume i1 <= i19;
        then G*(i19,j19)`1 >= G*(i1,j1)`1 by A25,A8,A12,A104,A105,A106,
SPRECT_3:13;
        hence contradiction by A21,A28,A45,A39,A4,A91,A95,A97,A96,A101,
GOBOARD5:3;
      end;
A108: G*(i2,j19)`1 = G*(i2,1)`1 by A14,A13,A103,GOBOARD5:2;
      now
        assume i2 >= i19;
        then G*(i2,j2)`1 >= G*(i19,j19)`1 by A13,A102,A103,A99,A108,SPRECT_3:13
;
        hence contradiction by A23,A42,A40,A33,A6,A34,A92,A95,A97,A98,A101,
GOBOARD5:3;
      end;
      hence contradiction by A89,A107,NAT_1:13;
    end;
    now
      assume m <= i;
      then
A109: F*(i,j)`1 >= F*(m,k)`1 by A24,A45,A39,A36,A43,A46,SPRECT_3:13;
      i1 > i2 by A89,NAT_1:13;
      hence contradiction by A21,A23,A4,A6,A18,A8,A12,A14,A89,A109,GOBOARD5:3;
    end;
    then i+1 <= m by NAT_1:13;
    then i+1 = m by A90,XXREAL_0:1;
    then
A110: right_cell(f,n) = cell(F,i,j) & left_cell(f,n) = cell(F,i,j-'1) by A1,A20
,A21,A22,A23,A35,A34,GOBOARD5:def 6,def 7;
    right_cell(f,n,G) = cell(G,i2,j2) & left_cell(f,n,G) = cell(G,i2,j2
    -'1) by A1,A2,A3,A4,A5,A6,A10,A89,Def1,Def2;
    hence thesis by A19,A22,A23,A5,A6,A110,Th10,Th12;
  end;
  suppose
A111: i1 = i2 & j1 = j2+1;
A112: now
A113: G*(i2,j2)`2 = G*(1,j2)`2 by A14,A13,A16,A11,GOBOARD5:1;
      assume
A114: j+1 < k;
      then
A115: j+1 < width F by A39,XXREAL_0:2;
      then consider l,i9 such that
A116: l in dom f and
A117: [i9,j+1] in Indices F and
A118: f/.l = F*(i9,j+1) by JORDAN5D:8,NAT_1:12;
A119: F*(m,j+1)`2 = F*(1,j+1)`2 by A24,A28,A32,A115,GOBOARD5:1;
      1 <= i9 & i9 <= len F by A117,MATRIX_0:32;
      then
A120: F*(i9,j+1)`2 = F*(1,j+1)`2 by A32,A115,GOBOARD5:1;
      consider i19,j19 such that
A121: [i19,j19] in Indices G and
A122: f/.l = G*(i19,j19) by A2,A116,GOBOARD1:def 9;
A123: j19 <= width G by A121,MATRIX_0:32;
A124: 1 <= i19 & i19 <= len G by A121,MATRIX_0:32;
      then
A125: G*(i19,j1)`2 = G*(1,j1)`2 by A8,A12,GOBOARD5:1;
A126: now
        assume j1 <= j19;
        then G*(i19,j19)`2 >= G*(i1,j1)`2 by A8,A27,A124,A123,A125,SPRECT_3:12;
        hence
        contradiction by A21,A24,A28,A39,A4,A32,A114,A118,A120,A119,A122,
GOBOARD5:4;
      end;
A127: F*(i,j+1)`2 = F*(1,j+1)`2 by A42,A36,A32,A115,GOBOARD5:1;
A128: 1 <= j19 by A121,MATRIX_0:32;
A129: G*(i19,j2)`2 = G*(1,j2)`2 by A16,A11,A124,GOBOARD5:1;
      now
        assume j2 >= j19;
        then G*(i2,j2)`2 >= G*(i19,j19)`2 by A11,A124,A128,A113,A129,
SPRECT_3:12;
        hence contradiction by A23,A42,A36,A40,A6,A29,A115,A118,A120,A127,A122,
GOBOARD5:4;
      end;
      hence contradiction by A111,A126,NAT_1:13;
    end;
    now
      assume j >= k;
      then
A130: F*(i,j)`2 >= F*(m,k)`2 by A24,A28,A45,A33,A44,A41,SPRECT_3:12;
      j1 > j2 by A111,NAT_1:13;
      hence contradiction by A21,A23,A4,A6,A12,A14,A13,A16,A27,A15,A130,
GOBOARD5:4;
    end;
    then j+1 <= k by NAT_1:13;
    then j+1 = k by A112,XXREAL_0:1;
    then
A131: right_cell(f,n) = cell(F,m -'1,j) & left_cell(f,n) = cell(F,m,j) by A1
,A20,A21,A22,A23,A30,A29,GOBOARD5:def 6,def 7;
A132: now
      assume
A133: m <> i;
      per cases by A133,XXREAL_0:1;
      suppose
        m < i;
        hence contradiction by A21,A23,A24,A45,A39,A36,A43,A46,A4,A6,A26,A17
,A111,GOBOARD5:3;
      end;
      suppose
        m > i;
        hence contradiction by A21,A23,A28,A45,A39,A42,A43,A46,A4,A6,A26,A17
,A111,GOBOARD5:3;
      end;
    end;
    right_cell(f,n,G) = cell(G,i1-'1,j2) & left_cell(f,n,G) = cell(G,i1,
    j2) by A1,A2,A3,A4,A5,A6,A9,A111,Def1,Def2;
    hence thesis by A19,A22,A23,A5,A6,A111,A132,A131,Th10,Th11;
  end;
end;

definition
  let f,G,k;
  assume 1 <= k & k+1 <= len f & f is_sequence_on G;
  then consider i1,j1,i2,j2 being Nat such that
A1: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f/.
  ( k+1) = G*(i2,j2) and
A2: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2 or
  i1 = i2 & j1 = j2+1 by JORDAN8:3;
  func front_right_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,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 A2;
    suppose
A3:   i1 = i2 & j1+1 = j2;
      take cell(G,i2,j2);
      let i19,j19,i29,j29 be Nat;
      assume
A4:   [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19,
      j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A3,A4,GOBOARD1:5;
    end;
    suppose
A5:   i1+1 = i2 & j1 = j2;
      take cell(G,i2,j2-'1);
      let i19,j19,i29,j29 be Nat;
      assume
A6:   [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19,
      j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A5,A6,GOBOARD1:5;
    end;
    suppose
A7:   i1 = i2+1 & j1 = j2;
      take cell(G,i2-'1,j2);
      let i19,j19,i29,j29 be Nat;
      assume
A8:   [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A7,A8,GOBOARD1:5;
    end;
    suppose
A9:   i1 = i2 & j1 = j2+1;
      take cell(G,i2-'1,j2-'1);
      let i19,j19,i29,j29 be Nat;
      assume
A10:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A9,A10,GOBOARD1:5;
    end;
  end;
  uniqueness
  proof
    let P1,P2 be Subset of TOP-REAL 2 such that
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 & 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
A12: 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 A2;
    suppose
A13:  i1 = i2 & j1+1 = j2;
A14:  j2 <= j2+1 by NAT_1:11;
A15:  j1 < j2 by A13,XREAL_1:29;
      hence P1 = cell(G,i2,j2) by A1,A11,A14
        .= P2 by A1,A12,A15,A14;
    end;
    suppose
A16:  i1+1 = i2 & j1 = j2;
A17:  i2 <= i2+1 by NAT_1:11;
A18:  i1 < i2 by A16,XREAL_1:29;
      hence P1 = cell(G,i2,j2-'1) by A1,A11,A17
        .= P2 by A1,A12,A18,A17;
    end;
    suppose
A19:  i1 = i2+1 & j1 = j2;
A20:  i1 <= i1+1 by NAT_1:11;
A21:  i2 < i1 by A19,XREAL_1:29;
      hence P1 = cell(G,i2-'1,j2) by A1,A11,A20
        .= P2 by A1,A12,A21,A20;
    end;
    suppose
A22:  i1 = i2 & j1 = j2+1;
A23:  j1 <= j1+1 by NAT_1:11;
A24:  j2 < j1 by A22,XREAL_1:29;
      hence P1 = cell(G,i2-'1,j2-'1) by A1,A11,A23
        .= P2 by A1,A12,A24,A23;
    end;
  end;
  func front_left_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
-'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 A2;
    suppose
A25:  i1 = i2 & j1+1 = j2;
      take cell(G,i2-'1,j2);
      let i19,j19,i29,j29 be Nat;
      assume
A26:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A25,A26,GOBOARD1:5;
    end;
    suppose
A27:  i1+1 = i2 & j1 = j2;
      take cell(G,i2,j2);
      let i19,j19,i29,j29 be Nat;
      assume
A28:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A27,A28,GOBOARD1:5;
    end;
    suppose
A29:  i1 = i2+1 & j1 = j2;
      take cell(G,i2-'1,j2-'1);
      let i19,j19,i29,j29 be Nat;
      assume
A30:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A29,A30,GOBOARD1:5;
    end;
    suppose
A31:  i1 = i2 & j1 = j2+1;
      take cell(G,i2,j2-'1);
      let i19,j19,i29,j29 be Nat;
      assume
A32:  [i19,j19] in Indices G & [i29,j29] in Indices G & f/.k = G*(i19
      ,j19) & f/.(k+1) = G*(i29,j29);
      then i2 = i29 & j1 = j19 by A1,GOBOARD1:5;
      hence thesis by A1,A31,A32,GOBOARD1:5;
    end;
  end;
  uniqueness
  proof
    let P1,P2 be Subset of TOP-REAL 2 such that
A33: 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
A34: 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 A2;
    suppose
A35:  i1 = i2 & j1+1 = j2;
A36:  j2 <= j2+1 by NAT_1:11;
A37:  j1 < j2 by A35,XREAL_1:29;
      hence P1 = cell(G,i2-'1,j2) by A1,A33,A36
        .= P2 by A1,A34,A37,A36;
    end;
    suppose
A38:  i1+1 = i2 & j1 = j2;
A39:  i2 <= i2+1 by NAT_1:11;
A40:  i1 < i2 by A38,XREAL_1:29;
      hence P1 = cell(G,i2,j2) by A1,A33,A39
        .= P2 by A1,A34,A40,A39;
    end;
    suppose
A41:  i1 = i2+1 & j1 = j2;
A42:  i1 <= i1+1 by NAT_1:11;
A43:  i2 < i1 by A41,XREAL_1:29;
      hence P1 = cell(G,i2-'1,j2-'1) by A1,A33,A42
        .= P2 by A1,A34,A43,A42;
    end;
    suppose
A44:  i1 = i2 & j1 = j2+1;
A45:  j1 <= j1+1 by NAT_1:11;
A46:  j2 < j1 by A44,XREAL_1:29;
      hence P1 = cell(G,i2,j2-'1) by A1,A33,A45
        .= P2 by A1,A34,A46,A45;
    end;
  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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def4;
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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def3;
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
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,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_right_cell(f,k,G) = cell(G,i+1,j-'1)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def3;
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
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,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_right_cell(f,k,G) = cell(G,i-'1,j)
proof
A1: i < i+1 & i+1 <= i+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def3;
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
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,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_right_cell(f,k,G) = cell(G,i-'1,j-'1)
proof
A1: j < j+1 & j+1 <= j+1+1 by XREAL_1:29;
  assume 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);
  hence thesis by A1,Def3;
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 and
A2: k+1 <= len f and
A3: f is_sequence_on G and
A4: k+1 <= n;
  per cases;
  suppose
    len f <= n;
    hence thesis by FINSEQ_1:58;
  end;
  suppose
    n < len f;
    then
A5: len(f|n) = n by FINSEQ_1:59;
    then k in dom(f|n) by A1,A4,SEQ_4:134;
    then
A6: (f|n)/.k = f/.k by FINSEQ_4:70;
    k+1 in dom(f|n) by A1,A4,A5,SEQ_4:134;
    then
A7: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
    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);
A8: f|n is_sequence_on G by A3,GOBOARD1:22;
    consider i1,j1,i2,j2 being Nat such that
A9: [i1,j1] in Indices G & f/.k = G*(i1,j1) & [i2,j2] in Indices G & f
    /.( k+1) = G*(i2,j2) and
A10: 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,A3,JORDAN8:3;
A11: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A12: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
    now
      per cases by A10;
      suppose
A13:    i1 = i2 & j1+1 = j2;
        hence lf = cell(G,i2-'1,j2) by A1,A2,A3,A9,A11,Def4
          .= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def4;
        thus rf = cell(G,i2,j2) by A1,A2,A3,A9,A11,A13,Def3
          .= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A13,Def3;
      end;
      suppose
A14:    i1+1 = i2 & j1 = j2;
        hence lf = cell(G,i2,j2) by A1,A2,A3,A9,A12,Def4
          .= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def4;
        thus rf = cell(G,i2,j2-'1) by A1,A2,A3,A9,A12,A14,Def3
          .= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A14,Def3;
      end;
      suppose
A15:    i1 = i2+1 & j1 = j2;
        hence lf = cell(G,i2-'1,j2-'1) by A1,A2,A3,A9,A12,Def4
          .= lfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def4;
        thus rf = cell(G,i2-'1,j2) by A1,A2,A3,A9,A12,A15,Def3
          .= rfn by A1,A4,A9,A12,A8,A5,A6,A7,A15,Def3;
      end;
      suppose
A16:    i1 = i2 & j1 = j2+1;
        hence lf = cell(G,i2,j2-'1) by A1,A2,A3,A9,A11,Def4
          .= lfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def4;
        thus rf = cell(G,i2-'1,j2-'1) by A1,A2,A3,A9,A11,A16,Def3
          .= rfn by A1,A4,A9,A11,A8,A5,A6,A7,A16,Def3;
      end;
    end;
    hence thesis;
  end;
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

  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

  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

  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 <= n & f|n turns_right k,G implies f turns_right k,G
proof
  assume that
A1: 1 <= k & k+2 <= n and
A2: f|n turns_right k,G;
  per cases;
  suppose
    len f <= n;
    hence thesis by A2,FINSEQ_1:58;
  end;
  suppose
A3: n < len f;
    let i19,j19,i29,j29 be Nat;
A4: len(f|n) = n by A3,FINSEQ_1:59;
    then k+1 in dom(f|n) by A1,SEQ_4:135;
    then
A5: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
    k+2 in dom(f|n) by A1,A4,SEQ_4:135;
    then
A6: (f|n)/.(k+2) = f/.(k+2 ) by FINSEQ_4:70;
    k in dom(f|n) by A1,A4,SEQ_4:135;
    then (f|n)/.k = f/.k by FINSEQ_4:70;
    hence thesis by A2,A5,A6;
  end;
end;

theorem
  1 <= k & k+2 <= n & f|n turns_left k,G implies f turns_left k,G
proof
  assume that
A1: 1 <= k & k+2 <= n and
A2: f|n turns_left k,G;
  per cases;
  suppose
    len f <= n;
    hence thesis by A2,FINSEQ_1:58;
  end;
  suppose
A3: n < len f;
    let i19,j19,i29,j29 be Nat;
A4: len(f|n) = n by A3,FINSEQ_1:59;
    then k+1 in dom(f|n) by A1,SEQ_4:135;
    then
A5: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
    k+2 in dom(f|n) by A1,A4,SEQ_4:135;
    then
A6: (f|n)/.(k+2) = f/.(k+2 ) by FINSEQ_4:70;
    k in dom(f|n) by A1,A4,SEQ_4:135;
    then (f|n)/.k = f/.k by FINSEQ_4:70;
    hence thesis by A2,A5,A6;
  end;
end;

theorem
  1 <= k & k+2 <= n & f|n goes_straight k,G implies f goes_straight k,G
proof
  assume that
A1: 1 <= k & k+2 <= n and
A2: f|n goes_straight k,G;
  per cases;
  suppose
    len f <= n;
    hence thesis by A2,FINSEQ_1:58;
  end;
  suppose
A3: n < len f;
    let i19,j19,i29,j29 be Nat;
A4: len(f|n) = n by A3,FINSEQ_1:59;
    then k+1 in dom(f|n) by A1,SEQ_4:135;
    then
A5: (f|n)/.(k+1) = f/.(k+1) by FINSEQ_4:70;
    k+2 in dom(f|n) by A1,A4,SEQ_4:135;
    then
A6: (f|n)/.(k+2) = f/.(k+2 ) by FINSEQ_4:70;
    k in dom(f|n) by A1,A4,SEQ_4:135;
    then (f|n)/.k = f/.k by FINSEQ_4:70;
    hence thesis by A2,A5,A6;
  end;
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 and
A2: k+1 <= len f1 and
A3: k+1 <= len f2 and
A4: f1 is_sequence_on G and
A5: f1|k = f2|k and
A6: f1 turns_right k-'1,G and
A7: f2 turns_right k-'1,G;
A8: 1 <= k-'1 by A1,NAT_D:49;
A9: k <= k+1 by NAT_1:12;
  then k <= len(f1|k) by A2,FINSEQ_1:59,XXREAL_0:2;
  then
A10: k in dom(f1|k) by A1,FINSEQ_3:25;
  then
A11: f2/.k = (f2|k)/.k by A5,FINSEQ_4:70;
  k-'1 <= k by NAT_D:35;
  then k-'1 <= len(f1|k) by A2,A9,FINSEQ_1:59,XXREAL_0:2;
  then
A12: k-'1 in dom(f1|k) by A8,FINSEQ_3:25;
  then
A13: f2/.(k-'1) = (f2|k)/.(k-'1) by A5,FINSEQ_4:70;
A14: f1/.k = (f1|k)/.k by A10,FINSEQ_4:70;
A15: f1/.(k-'1) = (f1|k)/.(k-'1) by A12,FINSEQ_4:70;
A16: k = k-'1+1 by A1,XREAL_1:235;
  k <= len f1 by A2,A9,XXREAL_0:2;
  then consider i1,j1,i2,j2 being Nat such that
A17: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) & [i2,j2] in Indices
  G & f1/.k = G*(i2,j2) and
A18: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
  or i1 = i2 & j1 = j2+1 by A4,A8,A16,JORDAN8:3;
A19: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A20: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
  now
    per cases by A18;
    suppose
A21:  i1 = i2 & j1+1 = j2;
      hence f1/.(k+1) = G*(i2+1,j2) by A6,A16,A17,A19
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A21;
    end;
    suppose
A22:  i1+1 = i2 & j1 = j2;
      hence f1/.(k+1) = G*(i2,j2-'1) by A6,A16,A17,A20
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A22;
    end;
    suppose
A23:  i1 = i2+1 & j1 = j2;
      hence f1/.(k+1) = G*(i2,j2+1) by A6,A16,A17,A20
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A23;
    end;
    suppose
A24:  i1 = i2 & j1 = j2+1;
      hence f1/.(k+1) = G*(i2-'1,j2) by A6,A16,A17,A19
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A24;
    end;
  end;
  hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A2,A5,FINSEQ_5:82
    .= f2|(k+1) by A3,FINSEQ_5:82;
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 and
A2: k+1 <= len f1 and
A3: k+1 <= len f2 and
A4: f1 is_sequence_on G and
A5: f1|k = f2|k and
A6: f1 turns_left k-'1,G and
A7: f2 turns_left k-'1,G;
A8: 1 <= k-'1 by A1,NAT_D:49;
A9: k <= k+1 by NAT_1:12;
  then k <= len(f1|k) by A2,FINSEQ_1:59,XXREAL_0:2;
  then
A10: k in dom(f1|k) by A1,FINSEQ_3:25;
  then
A11: f2/.k = (f2|k)/.k by A5,FINSEQ_4:70;
  k-'1 <= k by NAT_D:35;
  then k-'1 <= len(f1|k) by A2,A9,FINSEQ_1:59,XXREAL_0:2;
  then
A12: k-'1 in dom(f1|k) by A8,FINSEQ_3:25;
  then
A13: f2/.(k-'1) = (f2|k)/.(k-'1) by A5,FINSEQ_4:70;
A14: f1/.k = (f1|k)/.k by A10,FINSEQ_4:70;
A15: f1/.(k-'1) = (f1|k)/.(k-'1) by A12,FINSEQ_4:70;
A16: k = k-'1+1 by A1,XREAL_1:235;
  k <= len f1 by A2,A9,XXREAL_0:2;
  then consider i1,j1,i2,j2 being Nat such that
A17: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) & [i2,j2] in Indices
  G & f1/.k = G*(i2,j2) and
A18: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
  or i1 = i2 & j1 = j2+1 by A4,A8,A16,JORDAN8:3;
A19: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A20: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
  now
    per cases by A18;
    suppose
A21:  i1 = i2 & j1+1 = j2;
      hence f1/.(k+1) = G*(i2-'1,j2) by A6,A16,A17,A19
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A21;
    end;
    suppose
A22:  i1+1 = i2 & j1 = j2;
      hence f1/.(k+1) = G*(i2,j2+1) by A6,A16,A17,A20
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A22;
    end;
    suppose
A23:  i1 = i2+1 & j1 = j2;
      hence f1/.(k+1) = G*(i2,j2-'1) by A6,A16,A17,A20
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A23;
    end;
    suppose
A24:  i1 = i2 & j1 = j2+1;
      hence f1/.(k+1) = G*(i2+1,j2) by A6,A16,A17,A19
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A24;
    end;
  end;
  hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A2,A5,FINSEQ_5:82
    .= f2|(k+1) by A3,FINSEQ_5:82;
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 and
A2: k+1 <= len f1 and
A3: k+1 <= len f2 and
A4: f1 is_sequence_on G and
A5: f1|k = f2|k and
A6: f1 goes_straight k-'1,G and
A7: f2 goes_straight k-'1,G;
A8: 1 <= k-'1 by A1,NAT_D:49;
A9: k <= k+1 by NAT_1:12;
  then k <= len(f1|k) by A2,FINSEQ_1:59,XXREAL_0:2;
  then
A10: k in dom(f1|k) by A1,FINSEQ_3:25;
  then
A11: f2/.k = (f2|k)/.k by A5,FINSEQ_4:70;
  k-'1 <= k by NAT_D:35;
  then k-'1 <= len(f1|k) by A2,A9,FINSEQ_1:59,XXREAL_0:2;
  then
A12: k-'1 in dom(f1|k) by A8,FINSEQ_3:25;
  then
A13: f2/.(k-'1) = (f2|k)/.(k-'1) by A5,FINSEQ_4:70;
A14: f1/.k = (f1|k)/.k by A10,FINSEQ_4:70;
A15: f1/.(k-'1) = (f1|k)/.(k-'1) by A12,FINSEQ_4:70;
A16: k = k-'1+1 by A1,XREAL_1:235;
  k <= len f1 by A2,A9,XXREAL_0:2;
  then consider i1,j1,i2,j2 being Nat such that
A17: [i1,j1] in Indices G & f1/.(k-'1) = G*(i1,j1) & [i2,j2] in Indices
  G & f1/.k = G*(i2,j2) and
A18: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
  or i1 = i2 & j1 = j2+1 by A4,A8,A16,JORDAN8:3;
A19: j1+1 > j1 & j2+1 > j2 by NAT_1:13;
A20: i1+1 > i1 & i2+1 > i2 by NAT_1:13;
  now
    per cases by A18;
    suppose
A21:  i1 = i2 & j1+1 = j2;
      hence f1/.(k+1) = G*(i2,j2+1) by A6,A16,A17,A19
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A21;
    end;
    suppose
A22:  i1+1 = i2 & j1 = j2;
      hence f1/.(k+1) = G*(i2+1,j2) by A6,A16,A17,A20
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A22;
    end;
    suppose
A23:  i1 = i2+1 & j1 = j2;
      hence f1/.(k+1) = G*(i2-'1,j2) by A6,A16,A17,A20
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A20,A23;
    end;
    suppose
A24:  i1 = i2 & j1 = j2+1;
      hence f1/.(k+1) = G*(i2,j2-'1) by A6,A16,A17,A19
        .= f2/.(k+1) by A5,A7,A16,A15,A14,A13,A11,A17,A19,A24;
    end;
  end;
  hence f1|(k+1) = (f2|k)^<*f2/.(k+1)*> by A2,A5,FINSEQ_5:82
    .= f2|(k+1) by A3,FINSEQ_5:82;
end;