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) )
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) ) ; :: thesis: 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:8;
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:27;
then A12: fs1 /. 1 = i by A4, PARTFUN1:def 8;
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:27;
then A14: j2 = fs2 /. (len fs1) by A7, A8, PARTFUN1:def 8;
1 in dom fs2 by A8, A9, A10, FINSEQ_3:27;
then A15: fs2 /. 1 = j by A6, PARTFUN1:def 8;
A16: len fs1 in dom fs1 by A9, A13, FINSEQ_3:27;
then i2 = fs1 /. (len fs1) by A5, PARTFUN1:def 8;
hence Int (cell (GoB f),i,j) c= (LeftComp f) \/ (RightComp f) by A2, A3, A8, A16, A14, A11, A12, A15, Th8; :: thesis: verum