theorem Th34: :: JORDAN4:34

for f being constant standard special_circular_sequence
for i1, i2 being Nat st 1 <= i1 & i1 < i2 & i2 < len f holds
(mid (f,i1,1)) ^ (mid (f,((len f) -' 1),i2)) is_a_part<_of f,i1,i2