let m be Element of 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 Element of NAT st n in dom f holds
ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * i,j ) and
A2: for n being Element of NAT st n in dom f & n + 1 in dom f holds
for m, k, i, j being Element of NAT st [m,k] in Indices G & [i,j] in Indices G & f /. n = G * m,k & f /. (n + 1) = G * i,j holds
(abs (m - i)) + (abs (k - j)) = 1 ; :: according to GOBOARD1:def 11 :: thesis: f /^ m is_sequence_on G
set g = f /^ m;

hereby :: according to GOBOARD1:def 11 :: thesis: for b₁ being Element of NAT holds
( not b₁ in dom (f /^ m) or not b₁ + 1 in dom (f /^ m) or for b₂, b₃, b₄, b₅ being Element of NAT 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 (abs (b₂ - b₄)) + (abs (b₃ - b₅)) = 1 ) )

let n be Element of NAT ; :: thesis: ( n in dom (f /^ m) implies ex i, j being Element of 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 Element of NAT st
( [i,j] in Indices G & (f /^ m) /. n = G * i,j )
then n + m in dom f by FINSEQ_5:29;
then consider i, j being Element of NAT such that
A4: [i,j] in Indices G and
A5: f /. (n + m) = G * i,j by A1;
take i = i; :: thesis: ex j being Element of 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:30; :: thesis: verum

end;

let n be Element of NAT ; :: thesis: ( not n in dom (f /^ m) or not n + 1 in dom (f /^ m) or for b₁, b₂, b₃, b₄ being Element of NAT 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 (abs (b₁ - b₃)) + (abs (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 Element of NAT 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 (abs (b₁ - b₃)) + (abs (b₂ - b₄)) = 1 )
let i1, j1, i2, j2 be Element of 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 (abs (i1 - i2)) + (abs (j1 - j2)) = 1 )
assume that
A8: ( [i1,j1] in Indices G & [i2,j2] in Indices G ) and
A9: ( (f /^ m) /. n = G * i1,j1 & (f /^ m) /. (n + 1) = G * i2,j2 ) ; :: thesis: (abs (i1 - i2)) + (abs (j1 - j2)) = 1
A10: n + m in dom f by A6, FINSEQ_5:29;
A11: (n + 1) + m = (n + m) + 1 ;
then A12: (n + m) + 1 in dom f by A7, FINSEQ_5:29;
( f /. (n + m) = (f /^ m) /. n & f /. ((n + m) + 1) = (f /^ m) /. (n + 1) ) by A6, A7, A11, FINSEQ_5:30;
hence (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A2, A8, A9, A10, A12; :: thesis: verum