theorem Th7: :: GOBRD12:7

for f being non constant standard special_circular_sequence
for F1, F2 being FinSequence of NAT st len F1 = len F2 & ex i being Nat st
( i in dom F1 & Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f) ) & ( for i, k1, k2 being Nat st i in dom F1 & k1 = F1 . i & k2 = F2 . i holds
( k1 <= len (GoB f) & k2 <= width (GoB f) ) ) holds
for i being Nat st i in dom F1 holds
Int (cell ((GoB f),(F1 /. i),(F2 /. i))) c= (LeftComp f) \/ (RightComp f)