let f be non constant standard special_circular_sequence; :: thesis: 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 ; :: thesis: ( i <= len (GoB f) & j <= width (GoB f) implies Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f) )
assume A1: ( i <= len (GoB f) & j <= width (GoB f) ) ; :: thesis: 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
A2: ( i2 <= len (GoB f) & j2 <= width (GoB f) & Int (cell (GoB f),i2,j2) c= (LeftComp f) \/ (RightComp f) ) by Th9;
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) ) ) & fs1 . 1 = i & fs1 . (len fs1) = i2 & fs2 . 1 = j & fs2 . (len fs2) = j2 & len fs1 = len fs2 & len fs1 = ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) + 1 & ( 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, A2, GOBRD10:8;
A4: 1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) by NAT_1:12;
then A5: len fs1 in dom fs1 by A3, FINSEQ_3:27;
len fs2 in dom fs2 by A3, A4, FINSEQ_3:27;
then A6: ( i2 = fs1 /. (len fs1) & j2 = fs2 /. (len fs1) ) by A3, A5, PARTFUN1:def 8;
1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j)) by NAT_1:12;
then A7: ( 1 in dom fs1 & 1 in dom fs2 ) by A3, FINSEQ_3:27;
then ( fs1 /. 1 = i & fs2 /. 1 = j ) by A3, PARTFUN1:def 8;
hence Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f) by A2, A3, A5, A6, A7, Th8; :: thesis: verum