let m be Nat; :: thesis: for D being non empty set
for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
let D be non empty set ; :: thesis: for f being FinSequence of D
for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
let f be FinSequence of D; :: thesis: for G being Matrix of D st f is_sequence_on G holds
f /^ m is_sequence_on G
let G be Matrix of D; :: thesis: ( f is_sequence_on G implies f /^ m is_sequence_on G )
assume that
A1: for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) ) and
A2: for n being Nat st n in dom f & n + 1 in dom f holds
for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 ; :: according to GOBOARD1:def 9 :: thesis: f /^ m is_sequence_on G
set g = f /^ m;

hereby :: according to GOBOARD1:def 9 :: thesis: for b₁ being set holds
( not b₁ in dom (f /^ m) or not b₁ + 1 in dom (f /^ m) or for b₂, b₃, b₄, b₅ being set holds
( not [b₂,b₃] in Indices G or not [b₄,b₅] in Indices G or not (f /^ m) /. b₁ = G * (b₂,b₃) or not (f /^ m) /. (b₁ + 1) = G * (b₄,b₅) or |.(b₂ - b₄).| + |.(b₃ - b₅).| = 1 ) )

let n be Nat; :: thesis: ( n in dom (f /^ m) implies ex i, j being Nat st
( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) ) )
assume A3: n in dom (f /^ m) ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) )
then consider i, j being Nat such that
A4: [i,j] in Indices G and
A5: f /. (n + m) = G * (i,j) by A1, FINSEQ_5:26;
take i = i; :: thesis: ex j being Nat st
( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) )
take j = j; :: thesis: ( [i,j] in Indices G & (f /^ m) /. n = G * (i,j) )
thus [i,j] in Indices G by A4; :: thesis: (f /^ m) /. n = G * (i,j)
thus (f /^ m) /. n = G * (i,j) by A3, A5, FINSEQ_5:27; :: thesis: verum

end;

let n be Nat; :: thesis: ( not n in dom (f /^ m) or not n + 1 in dom (f /^ m) or for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in Indices G or not [b₃,b₄] in Indices G or not (f /^ m) /. n = G * (b₁,b₂) or not (f /^ m) /. (n + 1) = G * (b₃,b₄) or |.(b₁ - b₃).| + |.(b₂ - b₄).| = 1 ) )
assume that
A6: n in dom (f /^ m) and
A7: n + 1 in dom (f /^ m) ; :: thesis: for b₁, b₂, b₃, b₄ being set holds
( not [b₁,b₂] in Indices G or not [b₃,b₄] in Indices G or not (f /^ m) /. n = G * (b₁,b₂) or not (f /^ m) /. (n + 1) = G * (b₃,b₄) or |.(b₁ - b₃).| + |.(b₂ - b₄).| = 1 )
let i1, j1, i2, j2 be Nat; :: thesis: ( not [i1,j1] in Indices G or not [i2,j2] in Indices G or not (f /^ m) /. n = G * (i1,j1) or not (f /^ m) /. (n + 1) = G * (i2,j2) or |.(i1 - i2).| + |.(j1 - j2).| = 1 )
assume that
A8: [i1,j1] in Indices G and
A9: [i2,j2] in Indices G and
A10: (f /^ m) /. n = G * (i1,j1) and
A11: (f /^ m) /. (n + 1) = G * (i2,j2) ; :: thesis: |.(i1 - i2).| + |.(j1 - j2).| = 1
A12: n + m in dom f by A6, FINSEQ_5:26;
A13: (n + 1) + m = (n + m) + 1 ;
then A14: (n + m) + 1 in dom f by A7, FINSEQ_5:26;
A15: f /. (n + m) = (f /^ m) /. n by A6, FINSEQ_5:27;
f /. ((n + m) + 1) = (f /^ m) /. (n + 1) by A7, A13, FINSEQ_5:27;
hence |.(i1 - i2).| + |.(j1 - j2).| = 1 by A2, A8, A9, A10, A11, A12, A14, A15; :: thesis: verum