let k be Element of NAT ; :: thesis:
let D be set ; :: thesis:
let f be FinSequence of D; :: thesis:
let G be Matrix of D; :: thesis:
assume that
A1: ( 1 <= k & k + 1 <= len f ) and
A2: f is_sequence_on G ; :: thesis:
k <= k + 1 by NAT_1:11;
then k <= len f by A1, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A4: ( [i1,j1] in Indices G & f /. k = G * i1,j1 ) by A2, GOBOARD1:def 11;
k + 1 >= 1 by NAT_1:11;
then A5: k + 1 in dom f by A1, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A6: ( [i2,j2] in Indices G & f /. (k + 1) = G * i2,j2 ) by A2, GOBOARD1:def 11;
A7: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A3, A4, A5, A6, GOBOARD1:def 11;

per cases by A7, GOBOARD1:2;

case that A8: abs (i1 - i2) = 1 and
A9: j1 = j2 ; :: thesis:

( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A8, ABSVALUE:def 1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; :: thesis:
thus j1 = j2 by A9; :: thesis:

end;

case that A10: i1 = i2 and
A11: abs (j1 - j2) = 1 ; :: thesis:

( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A11, ABSVALUE:def 1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; :: thesis:
thus i1 = i2 by A10; :: thesis:

end;

hence ex i1, j1, i2, j2 being Element of 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 ) ) ) by A4, A6; :: thesis: