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
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:
consider i1 being Element of NAT such that
A4: i1 in dom F1 and
A5: 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 ;
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 6;
A7: F1 /. i1 = F1 . i1 by A4, PARTFUN1:def 6;
then kw1 <= len (GoB f) by A3, A4, A6;
then A8: k1 <= (len (GoB f)) + 1 by XREAL_1:6;
kw2 <= width (GoB f) by A3, A4, A7, A6;
then A9: k2 <= (width (GoB f)) + 1 by XREAL_1:6;
A10: ( k1 -' 1 = F1 /. i1 & k2 -' 1 = F2 /. i1 ) by NAT_D:34;
set n = len (GoB f);
set m = width (GoB f);
defpred S₁[ Nat, Nat, set ] means $3 = Int (cell ((GoB f),($1 -' 1),($2 -' 1)));
reconsider F = (LeftComp f) \/ (RightComp f) as Subset of (REAL 2) by EUCLID:22;
A12: 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(A12);
then consider Mm being Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1, bool (REAL 2) such that
A13: for i, j being Nat st [i,j] in Indices Mm holds
Mm * (i,j) = Int (cell ((GoB f),(i -' 1),(j -' 1))) ;
A14: len Mm = (len (GoB f)) + 1 by MATRIX_1:def 2;
then A15: dom Mm = Seg ((len (GoB f)) + 1) by FINSEQ_1:def 3;
A16: Seg ((width (GoB f)) + 1) = Seg (width Mm) by A14, MATRIX_1:20;
A17: (width (GoB f)) + 1 = width Mm by A14, MATRIX_1:20;
A18: 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 that
A19: i1 in Seg ((len (GoB f)) + 1) and
A20: i2 in Seg ((len (GoB f)) + 1) and
A21: j1 in Seg ((width (GoB f)) + 1) and
A22: j2 in Seg ((width (GoB f)) + 1) and
A23: i1,j1,i2,j2 are_adjacent2 ; :: thesis:
A24: 1 <= i2 by A20, FINSEQ_1:1;
then 0 <= i2 - 1 by XREAL_1:48;
then A25: i2 -' 1 = i2 - 1 by XREAL_0:def 2;
[i2,j2] in [:(dom Mm),(Seg (width Mm)):] by A15, A16, A20, A22, ZFMISC_1:87;
then [i2,j2] in Indices Mm by MATRIX_1:def 4;
then A26: Mm * (i2,j2) = Int (cell ((GoB f),(i2 -' 1),(j2 -' 1))) by A13;
reconsider ii1 = i1 -' 1, ii2 = i2 -' 1, jj1 = j1 -' 1, jj2 = j2 -' 1 as Element of NAT ;
A27: 1 <= i1 by A19, FINSEQ_1:1;
then 0 <= i1 - 1 by XREAL_1:48;
then A28: i1 -' 1 = i1 - 1 by XREAL_0:def 2;
[i1,j1] in [:(dom Mm),(Seg (width Mm)):] by A15, A17, A19, A21, ZFMISC_1:87;
then [i1,j1] in Indices Mm by MATRIX_1:def 4;
then A29: Mm * (i1,j1) = Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A13;
A30: 1 <= j2 by A22, FINSEQ_1:1;
then 0 <= j2 - 1 by XREAL_1:48;
then A31: j2 -' 1 = j2 - 1 by XREAL_0:def 2;
i2 <= (len (GoB f)) + 1 by A20, FINSEQ_1:1;
then A32: i2 -' 1 <= ((len (GoB f)) + 1) - 1 by A25, XREAL_1:9;
A33: 1 <= j1 by A21, FINSEQ_1:1;
then 0 <= j1 - 1 by XREAL_1:48;
then A34: j1 -' 1 = j1 - 1 by XREAL_0:def 2;
j2 <= (width (GoB f)) + 1 by A22, FINSEQ_1:1;
then A35: j2 -' 1 <= ((width (GoB f)) + 1) - 1 by A31, XREAL_1:9;
j1 <= (width (GoB f)) + 1 by A21, FINSEQ_1:1;
then A36: j1 -' 1 <= ((width (GoB f)) + 1) - 1 by A34, XREAL_1:9;
i1 <= (len (GoB f)) + 1 by A19, FINSEQ_1:1;
then A37: i1 -' 1 <= ((len (GoB f)) + 1) - 1 by A28, XREAL_1:9;
ii1,jj1,ii2,jj2 are_adjacent2 by A23, A27, A24, A33, A30, GOBRD10:4;
hence ( Mm * (i1,j1) c= (LeftComp f) \/ (RightComp f) iff Mm * (i2,j2) c= (LeftComp f) \/ (RightComp f) ) by A37, A32, A36, A35, A29, A26, Th7; :: thesis:

end;

0 + 1 <= k2 by NAT_1:13;
then A38: k2 in Seg ((width (GoB f)) + 1) by A9, FINSEQ_1:1;
0 + 1 <= k1 by NAT_1:13;
then A39: k1 in Seg ((len (GoB f)) + 1) by A8, FINSEQ_1:1;
then [k1,k2] in [:(dom Mm),(Seg (width Mm)):] by A38, A15, A16, ZFMISC_1:87;
then [k1,k2] in Indices Mm by MATRIX_1:def 4;
then Mm * (k1,k2) c= (LeftComp f) \/ (RightComp f) by A5, A13, A10;
then A40: 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 A39, A38, A18, GOBRD10:8;
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 A41: 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 ;
dom F1 = Seg (len F1) by FINSEQ_1:def 3;
then dom F1 = dom F2 by A1, FINSEQ_1:def 3;
then A42: F2 /. i = F2 . i by A41, PARTFUN1:def 6;
A43: F1 /. i = F1 . i by A41, PARTFUN1:def 6;
then kx1 <= len (GoB f) by A3, A41, A42;
then A44: kk1 <= (len (GoB f)) + 1 by XREAL_1:6;
kx2 <= width (GoB f) by A3, A41, A43, A42;
then A45: kk2 <= (width (GoB f)) + 1 by XREAL_1:6;
0 + 1 <= kk2 by NAT_1:13;
then A46: kk2 in Seg ((width (GoB f)) + 1) by A45, FINSEQ_1:1;
0 + 1 <= kk1 by NAT_1:13;
then A47: kk1 in Seg ((len (GoB f)) + 1) by A44, FINSEQ_1:1;
len Mm = (len (GoB f)) + 1 by MATRIX_1:def 2;
then ( dom Mm = Seg ((len (GoB f)) + 1) & Seg ((width (GoB f)) + 1) = Seg (width Mm) ) by FINSEQ_1:def 3, MATRIX_1:20;
then [kk1,kk2] in [:(dom Mm),(Seg (width Mm)):] by A47, A46, ZFMISC_1:87;
then A48: [kk1,kk2] in Indices Mm by MATRIX_1:def 4;
A49: ( kk1 -' 1 = F1 /. i & kk2 -' 1 = F2 /. i ) by NAT_D:34;
Mm * (kk1,kk2) c= (LeftComp f) \/ (RightComp f) by A40, A47, A46;
hence Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) by A13, A49, A48; :: thesis:

end;