let f be non constant standard special_circular_sequence; for i, j being 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 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 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 Th8;
A3:
( i in NAT & j in NAT & i2 in NAT & j2 in NAT & len (GoB f) in NAT & width (GoB f) in NAT )
by ORDINAL1:def 12;
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
A4:
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
A5:
fs1 . 1 = i
and
A6:
fs1 . (len fs1) = i2
and
A7:
fs2 . 1 = j
and
A8:
fs2 . (len fs2) = j2
and
A9:
len fs1 = len fs2
and
A10:
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_adjacent
by A1, GOBRD10:7, A3;
A11:
for k, k1, k2 being Nat st k in dom fs1 & k1 = fs1 . k & k2 = fs2 . k holds
( k1 <= len (GoB f) & k2 <= width (GoB f) )
A12:
1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j))
by NAT_1:12;
then A13:
1 in dom fs1
by A10, FINSEQ_3:25;
then A14:
fs1 /. 1 = i
by A5, PARTFUN1:def 6;
A15:
1 <= 1 + ((((i -' i2) + (i2 -' i)) + (j -' j2)) + (j2 -' j))
by NAT_1:12;
then
len fs2 in dom fs2
by A9, A10, FINSEQ_3:25;
then A16:
j2 = fs2 /. (len fs1)
by A8, A9, PARTFUN1:def 6;
1 in dom fs2
by A9, A10, A12, FINSEQ_3:25;
then A17:
fs2 /. 1 = j
by A7, PARTFUN1:def 6;
A18:
len fs1 in dom fs1
by A10, A15, FINSEQ_3:25;
then
i2 = fs1 /. (len fs1)
by A6, PARTFUN1:def 6;
hence
Int (cell ((GoB f),i,j)) c= (LeftComp f) \/ (RightComp f)
by A2, A9, A18, A16, A13, A14, A17, Th7, A11; verum