theorem Th3: :: JORDAN8:3

for k being Nat

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

ex i1, j1, i2, j2 being Nat st

( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )

for D being set

for f being FinSequence of D

for G being Matrix of D st 1 <= k & k + 1 <= len f & f is_sequence_on G holds

ex i1, j1, i2, j2 being Nat st

( [i1,j1] in Indices G & f /. k = G * (i1,j1) & [i2,j2] in Indices G & f /. (k + 1) = G * (i2,j2) & ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) )