let f be non constant standard special_circular_sequence; for i, j being Element of NAT st i <= len (GoB f) & j <= width (GoB f) holds
Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f)
let i, j be Element of NAT ; ( i <= len (GoB f) & j <= width (GoB f) implies Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f) )
set n = len (GoB f);
set m = width (GoB f);
consider i2, j2 being Element of NAT such that
A1:
( i2 <= len (GoB f) & j2 <= width (GoB f) )
and
A2:
Int (cell ((GoB f),i2,j2)) c= (LeftComp f) \/ (RightComp f)
by Th9;
assume
( i <= len (GoB f) & j <= width (GoB f) )
; Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f)
then consider fs1, fs2 being FinSequence of NAT such that
A3:
for k, k1, k2 being Element of NAT st k in dom fs1 & k1 = fs1 . k & k2 = fs2 . k holds
( k1 <= len (GoB f) & k2 <= width (GoB f) )
and
A4:
fs1 . 1 = i
and
A5:
fs1 . (len fs1) = i2
and
A6:
fs2 . 1 = j
and
A7:
fs2 . (len fs2) = j2
and
A8:
len fs1 = len fs2
and
A9:
len fs1 = ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) + 1
and
for k being Element of NAT st 1 <= k & k < len fs1 holds
fs1 /. k,fs2 /. k,fs1 /. (k + 1),fs2 /. (k + 1) are_adjacent2
by A1, GOBRD10:7;
A10:
1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j))
by NAT_1:12;
then A11:
1 in dom fs1
by A9, FINSEQ_3:25;
then A12:
fs1 /. 1 = i
by A4, PARTFUN1:def 6;
A13:
1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j))
by NAT_1:12;
then
len fs2 in dom fs2
by A8, A9, FINSEQ_3:25;
then A14:
j2 = fs2 /. (len fs1)
by A7, A8, PARTFUN1:def 6;
1 in dom fs2
by A8, A9, A10, FINSEQ_3:25;
then A15:
fs2 /. 1 = j
by A6, PARTFUN1:def 6;
A16:
len fs1 in dom fs1
by A9, A13, FINSEQ_3:25;
then
i2 = fs1 /. (len fs1)
by A5, PARTFUN1:def 6;
hence
Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f)
by A2, A3, A8, A16, A14, A11, A12, A15, Th8; verum