let f be non constant standard special_circular_sequence; :: thesis: 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; :: 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 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) ) ; :: thesis: 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) )
proof
let k, k1, k2 be Nat; :: thesis: ( k in dom fs1 & k1 = fs1 . k & k2 = fs2 . k implies ( k1 <= len (GoB f) & k2 <= width (GoB f) ) )
( k in NAT & k1 in NAT & k2 in NAT ) by ORDINAL1:def 12;
hence ( k in dom fs1 & k1 = fs1 . k & k2 = fs2 . k implies ( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) by A4; :: thesis: verum
end;
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; :: thesis: verum