let k be Nat; :: thesis: 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 ) ) )
let D be set ; :: thesis: 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 ) ) )
let f be FinSequence of D; :: thesis: 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 ) ) )
let G be Matrix of D; :: thesis: ( 1 <= k & k + 1 <= len f & f is_sequence_on G implies 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 ) ) ) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f and
A3: f is_sequence_on G ; :: thesis: 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 ) ) )
k <= k + 1 by NAT_1:11;
then k <= len f by A2, XXREAL_0:2;
then A4: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A5: [i1,j1] in Indices G and
A6: f /. k = G * (i1,j1) by A3;
k + 1 >= 1 by NAT_1:11;
then A7: k + 1 in dom f by A2, FINSEQ_3:25;
then consider i2, j2 being Nat such that
A8: [i2,j2] in Indices G and
A9: f /. (k + 1) = G * (i2,j2) by A3;
A10: |.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A6, A7, A8, A9;
now :: thesis: ( ( |.(i1 - i2).| = 1 & j1 = j2 & ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 ) or ( i1 = i2 & |.(j1 - j2).| = 1 & ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 ) )
per cases ( ( |.(i1 - i2).| = 1 & j1 = j2 ) or ( i1 = i2 & |.(j1 - j2).| = 1 ) ) by A10, SEQM_3:42;
case that A11: |.(i1 - i2).| = 1 and
A12: j1 = j2 ; :: thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )
( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def 1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; :: thesis: j1 = j2
thus j1 = j2 by A12; :: thesis: verum
end;
case that A13: i1 = i2 and
A14: |.(j1 - j2).| = 1 ; :: thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )
( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def 1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; :: thesis: i1 = i2
thus i1 = i2 by A13; :: thesis: verum
end;
end;
end;
hence 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 ) ) ) by A5, A6, A8, A9; :: thesis: verum