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 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 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 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;
A11: 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_0:sch 2(A11);
then consider Mm being Matrix of (len (GoB f)) + 1,(width (GoB f)) + 1,(bool (REAL 2)) such that
A12: for i, j being Nat st [i,j] in Indices Mm holds
Mm * (i,j) = Int (cell ((GoB f),(i -' 1),(j -' 1))) ;
A13: len Mm = (len (GoB f)) + 1 by MATRIX_0:def 2;
then A14: dom Mm = Seg ((len (GoB f)) + 1) by FINSEQ_1:def 3;
A15: Seg ((width (GoB f)) + 1) = Seg (width Mm) by A13, MATRIX_0:20;
A16: (width (GoB f)) + 1 = width Mm by A13, MATRIX_0:20;
A17: 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_adjacent 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
A18: i1 in Seg ((len (GoB f)) + 1) and
A19: i2 in Seg ((len (GoB f)) + 1) and
A20: j1 in Seg ((width (GoB f)) + 1) and
A21: j2 in Seg ((width (GoB f)) + 1) and
A22: i1,j1,i2,j2 are_adjacent ; :: thesis:
A23: 1 <= i2 by A19, FINSEQ_1:1;
then 0 <= i2 - 1 by XREAL_1:48;
then A24: i2 -' 1 = i2 - 1 by XREAL_0:def 2;
[i2,j2] in [:(dom Mm),(Seg (width Mm)):] by A14, A15, A19, A21, ZFMISC_1:87;
then [i2,j2] in Indices Mm by MATRIX_0:def 4;
then A25: Mm * (i2,j2) = Int (cell ((GoB f),(i2 -' 1),(j2 -' 1))) by A12;
reconsider ii1 = i1 -' 1, ii2 = i2 -' 1, jj1 = j1 -' 1, jj2 = j2 -' 1 as Element of NAT ;
A26: 1 <= i1 by A18, FINSEQ_1:1;
then 0 <= i1 - 1 by XREAL_1:48;
then A27: i1 -' 1 = i1 - 1 by XREAL_0:def 2;
[i1,j1] in [:(dom Mm),(Seg (width Mm)):] by A14, A16, A18, A20, ZFMISC_1:87;
then [i1,j1] in Indices Mm by MATRIX_0:def 4;
then A28: Mm * (i1,j1) = Int (cell ((GoB f),(i1 -' 1),(j1 -' 1))) by A12;
A29: 1 <= j2 by A21, FINSEQ_1:1;
then 0 <= j2 - 1 by XREAL_1:48;
then A30: j2 -' 1 = j2 - 1 by XREAL_0:def 2;
i2 <= (len (GoB f)) + 1 by A19, FINSEQ_1:1;
then A31: i2 -' 1 <= ((len (GoB f)) + 1) - 1 by A24, XREAL_1:9;
A32: 1 <= j1 by A20, FINSEQ_1:1;
then 0 <= j1 - 1 by XREAL_1:48;
then A33: j1 -' 1 = j1 - 1 by XREAL_0:def 2;
j2 <= (width (GoB f)) + 1 by A21, FINSEQ_1:1;
then A34: j2 -' 1 <= ((width (GoB f)) + 1) - 1 by A30, XREAL_1:9;
j1 <= (width (GoB f)) + 1 by A20, FINSEQ_1:1;
then A35: j1 -' 1 <= ((width (GoB f)) + 1) - 1 by A33, XREAL_1:9;
i1 <= (len (GoB f)) + 1 by A18, FINSEQ_1:1;
then A36: i1 -' 1 <= ((len (GoB f)) + 1) - 1 by A27, XREAL_1:9;
ii1,jj1,ii2,jj2 are_adjacent by A22, A26, A23, A32, A29, GOBRD10:4;
hence ( Mm * (i1,j1) c= (LeftComp f) \/ (RightComp f) iff Mm * (i2,j2) c= (LeftComp f) \/ (RightComp f) ) by A36, A31, A35, A34, A28, A25, Th6; :: thesis:

end;

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

end;