let f be non constant standard special_circular_sequence; :: thesis:
let F1, F2 be FinSequence of NAT ; :: thesis:
assume that
A1: len F1 = len F2 and
A2: ex i being Element of NAT st
( i in dom F1 & Int (cell (GoB f),(F1 /. i),(F2 /. i)) c= (LeftComp f) \/ (RightComp f) ) and
for i being Element of NAT st 1 <= i & i < len F1 holds
F1 /. i,F2 /. i,F1 /. (i + 1),F2 /. (i + 1) are_adjacent2 and
A3: for i, k1, k2 being Element of NAT st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds
( k1 <= len (GoB f) & k2 <= width (GoB f) ) ; :: thesis:
reconsider F = (LeftComp f) \/ (RightComp f) as Subset of (REAL 2) by EUCLID:25;
consider i1 being Element of NAT such that
A4: ( i1 in dom F1 & Int (cell (GoB f),(F1 /. i1),(F2 /. i1)) c= (LeftComp f) \/ (RightComp f) ) by A2;
reconsider kw1 = F1 /. i1, kw2 = F2 /. i1 as Element of NAT ;
reconsider k1 = kw1 + 1, k2 = kw2 + 1 as Element of NAT ;
A5: F1 /. i1 = F1 . i1 by A4, PARTFUN1:def 8;
dom F1 = Seg (len F1) by FINSEQ_1:def 3;
then dom F1 = dom F2 by A1, FINSEQ_1:def 3;
then A6: F2 /. i1 = F2 . i1 by A4, PARTFUN1:def 8;
defpred S₁[ Nat, Nat, set ] means $3 = Int (cell (GoB f),($1 -' 1),($2 -' 1));
A7: for i, j being Nat st [i,j] in [:(Seg ((len (GoB f)) + 1)),(Seg ((width (GoB f)) + 1)):] holds
for x1, x2 being Subset of (REAL 2) st S₁[i,j,x1] & S₁[i,j,x2] holds
x1 = x2 ;
A8: for i, j being Nat st [i,j] in [:(Seg ((len (GoB f)) + 1)),(Seg ((width (GoB f)) + 1)):] holds
ex x being Subset of (REAL 2) st S₁[i,j,x] by Lm2;
ex Mm being Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2) st
for i, j being Nat st [i,j] in Indices Mm holds
S₁[i,j,Mm * i,j] from MATRIX_1:sch 2(A7, A8);
then consider Mm being Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2) such that
A9: for i, j being Nat st [i,j] in Indices Mm holds
Mm * i,j = Int (cell (GoB f),(i -' 1),(j -' 1)) ;
( kw1 <= len (GoB f) & kw2 <= width (GoB f) ) by A3, A4, A5, A6;
then A10: ( k1 <= (len (GoB f)) + 1 & k2 <= (width (GoB f)) + 1 ) by XREAL_1:8;
set n = len (GoB f);
set m = width (GoB f);
( 0 + 1 <= k1 & 0 + 1 <= k2 ) by NAT_1:13;
then A11: ( k1 in Seg ((len (GoB f)) + 1) & k2 in Seg ((width (GoB f)) + 1) ) by A10, FINSEQ_1:3;
A12: len Mm = (len (GoB f)) + 1 by MATRIX_1:def 3;
then A13: dom Mm = Seg ((len (GoB f)) + 1) by FINSEQ_1:def 3;
A14: (width (GoB f)) + 1 = width Mm by A12, MATRIX_1:20;
A15: Seg ((width (GoB f)) + 1) = Seg (width Mm) by A12, MATRIX_1:20;
A16: ( k1 -' 1 = F1 /. i1 & k2 -' 1 = F2 /. i1 ) by NAT_D:34;
[k1,k2] in [:(dom Mm),(Seg (width Mm)):] by A11, A13, A15, ZFMISC_1:106;
then [k1,k2] in Indices Mm by MATRIX_1:def 5;
then A17: Mm * k1,k2 c= (LeftComp f) \/ (RightComp f) by A4, A9, A16;
for i1, j1, i2, j2 being Element of NAT st i1 in Seg ((len (GoB f)) + 1) & i2 in Seg ((len (GoB f)) + 1) & j1 in Seg ((width (GoB f)) + 1) & j2 in Seg ((width (GoB f)) + 1) & i1,j1,i2,j2 are_adjacent2 holds
( Mm * i1,j1 c= (LeftComp f) \/ (RightComp f) iff Mm * i2,j2 c= (LeftComp f) \/ (RightComp f) )

proof

let i1, j1, i2, j2 be Element of NAT ; :: thesis:
assume A18: ( i1 in Seg ((len (GoB f)) + 1) & i2 in Seg ((len (GoB f)) + 1) & j1 in Seg ((width (GoB f)) + 1) & j2 in Seg ((width (GoB f)) + 1) & i1,j1,i2,j2 are_adjacent2 ) ; :: thesis:
reconsider ii1 = i1 -' 1, ii2 = i2 -' 1, jj1 = j1 -' 1, jj2 = j2 -' 1 as Element of NAT ;
A19: ( 1 <= i1 & i1 <= (len (GoB f)) + 1 ) by A18, FINSEQ_1:3;
A20: ( 1 <= i2 & i2 <= (len (GoB f)) + 1 ) by A18, FINSEQ_1:3;
A21: ( 1 <= j1 & j1 <= (width (GoB f)) + 1 ) by A18, FINSEQ_1:3;
A22: ( 1 <= j2 & j2 <= (width (GoB f)) + 1 ) by A18, FINSEQ_1:3;
0 <= i1 - 1 by A19, XREAL_1:50;
then i1 -' 1 = i1 - 1 by XREAL_0:def 2;
then A23: i1 -' 1 <= ((len (GoB f)) + 1) - 1 by A19, XREAL_1:11;
0 <= i2 - 1 by A20, XREAL_1:50;
then i2 -' 1 = i2 - 1 by XREAL_0:def 2;
then A24: i2 -' 1 <= ((len (GoB f)) + 1) - 1 by A20, XREAL_1:11;
0 <= j1 - 1 by A21, XREAL_1:50;
then j1 -' 1 = j1 - 1 by XREAL_0:def 2;
then A25: j1 -' 1 <= ((width (GoB f)) + 1) - 1 by A21, XREAL_1:11;
0 <= j2 - 1 by A22, XREAL_1:50;
then j2 -' 1 = j2 - 1 by XREAL_0:def 2;
then A26: j2 -' 1 <= ((width (GoB f)) + 1) - 1 by A22, XREAL_1:11;
A27: ii1,jj1,ii2,jj2 are_adjacent2 by A18, A19, A20, A21, A22, GOBRD10:4;
[i1,j1] in [:(dom Mm),(Seg (width Mm)):] by A13, A14, A18, ZFMISC_1:106;
then [i1,j1] in Indices Mm by MATRIX_1:def 5;
then A28: Mm * i1,j1 = Int (cell (GoB f),(i1 -' 1),(j1 -' 1)) by A9;
[i2,j2] in [:(dom Mm),(Seg (width Mm)):] by A13, A15, A18, ZFMISC_1:106;
then [i2,j2] in Indices Mm by MATRIX_1:def 5;
then Mm * i2,j2 = Int (cell (GoB f),(i2 -' 1),(j2 -' 1)) by A9;
hence ( Mm * i1,j1 c= (LeftComp f) \/ (RightComp f) iff Mm * i2,j2 c= (LeftComp f) \/ (RightComp f) ) by A23, A24, A25, A26, A27, A28, Th7; :: thesis:

end;

then A29: for i, j being Element of NAT st i in Seg ((len (GoB f)) + 1) & j in Seg ((width (GoB f)) + 1) holds
Mm * i,j c= F by A11, A17, GOBRD10:9;
thus for i being Element of NAT st i in dom F1 holds
Int (cell (GoB f),(F1 /. i),(F2 /. i)) c= (LeftComp f) \/ (RightComp f) :: thesis:

proof

let i be Element of NAT ; :: thesis:
assume A30: i in dom F1 ; :: thesis:
reconsider kx1 = F1 /. i, kx2 = F2 /. i as Element of NAT ;
reconsider kk1 = kx1 + 1, kk2 = kx2 + 1 as Element of NAT ;
A31: F1 /. i = F1 . i by A30, PARTFUN1:def 8;
dom F1 = Seg (len F1) by FINSEQ_1:def 3;
then dom F1 = dom F2 by A1, FINSEQ_1:def 3;
then F2 /. i = F2 . i by A30, PARTFUN1:def 8;
then ( kx1 <= len (GoB f) & kx2 <= width (GoB f) ) by A3, A30, A31;
then A32: ( kk1 <= (len (GoB f)) + 1 & kk2 <= (width (GoB f)) + 1 ) by XREAL_1:8;
( 0 + 1 <= kk1 & 0 + 1 <= kk2 ) by NAT_1:13;
then A33: ( kk1 in Seg ((len (GoB f)) + 1) & kk2 in Seg ((width (GoB f)) + 1) ) by A32, FINSEQ_1:3;
then A34: Mm * kk1,kk2 c= (LeftComp f) \/ (RightComp f) by A29;
A35: len Mm = (len (GoB f)) + 1 by MATRIX_1:def 3;
then A36: dom Mm = Seg ((len (GoB f)) + 1) by FINSEQ_1:def 3;
A37: Seg ((width (GoB f)) + 1) = Seg (width Mm) by A35, MATRIX_1:20;
A38: ( kk1 -' 1 = F1 /. i & kk2 -' 1 = F2 /. i ) by NAT_D:34;
[kk1,kk2] in [:(dom Mm),(Seg (width Mm)):] by A33, A36, A37, ZFMISC_1:106;
then [kk1,kk2] in Indices Mm by MATRIX_1:def 5;
hence Int (cell (GoB f),(F1 /. i),(F2 /. i)) c= (LeftComp f) \/ (RightComp f) by A9, A34, A38; :: thesis:

end;