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 b1 being set holds
( not b1 in dom (f /^ m) or not b1 + 1 in dom (f /^ m) or for b2, b3, b4, b5 being set holds
( not [b2,b3] in Indices G or not [b4,b5] in Indices G or not (f /^ m) /. b1 = G * (b2,b3) or not (f /^ m) /. (b1 + 1) = G * (b4,b5) or |.(b2 - b4).| + |.(b3 - b5).| = 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 b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not (f /^ m) /. n = G * (b1,b2) or not (f /^ m) /. (n + 1) = G * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 1 ) )
assume that
A6: n in dom (f /^ m) and
A7: n + 1 in dom (f /^ m) ; :: thesis: for b1, b2, b3, b4 being set holds
( not [b1,b2] in Indices G or not [b3,b4] in Indices G or not (f /^ m) /. n = G * (b1,b2) or not (f /^ m) /. (n + 1) = G * (b3,b4) or |.(b1 - b3).| + |.(b2 - b4).| = 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