let D be non empty set ; :: thesis: for G being Matrix of D
for f being FinSequence of D holds
( f is_sequence_on G iff Rev f is_sequence_on G )
let G be Matrix of D; :: thesis: for f being FinSequence of D holds
( f is_sequence_on G iff Rev f is_sequence_on G )
let f be FinSequence of D; :: thesis: ( f is_sequence_on G iff Rev f is_sequence_on G )

hereby :: thesis: ( Rev f is_sequence_on G implies f is_sequence_on G )

assume A1: f is_sequence_on G ; :: thesis: Rev f is_sequence_on G
A2: for n being Nat st n in dom (Rev f) & n + 1 in dom (Rev f) holds
for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & (Rev f) /. n = G * (m,k) & (Rev f) /. (n + 1) = G * (i,j) holds
|.(m - i).| + |.(k - j).| = 1

proof

let n be Nat; :: thesis: ( n in dom (Rev f) & n + 1 in dom (Rev f) implies for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & (Rev f) /. n = G * (m,k) & (Rev f) /. (n + 1) = G * (i,j) holds
|.(m - i).| + |.(k - j).| = 1 )
assume that
A3: n in dom (Rev f) and
A4: n + 1 in dom (Rev f) ; :: thesis: for m, k, i, j being Nat st [m,k] in Indices G & [i,j] in Indices G & (Rev f) /. n = G * (m,k) & (Rev f) /. (n + 1) = G * (i,j) holds
|.(m - i).| + |.(k - j).| = 1
consider l being Nat such that
A5: l in dom f and
A6: n + l = (len f) + 1 and
A7: (Rev f) /. n = f /. l by A3, Th4;
let m, k, i, j be Nat; :: thesis: ( [m,k] in Indices G & [i,j] in Indices G & (Rev f) /. n = G * (m,k) & (Rev f) /. (n + 1) = G * (i,j) implies |.(m - i).| + |.(k - j).| = 1 )
assume A8: ( [m,k] in Indices G & [i,j] in Indices G & (Rev f) /. n = G * (m,k) & (Rev f) /. (n + 1) = G * (i,j) ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A9: ( |.(i - m).| = |.(m - i).| & |.(j - k).| = |.(k - j).| ) by UNIFORM1:11;
consider l9 being Nat such that
A10: l9 in dom f and
A11: (n + 1) + l9 = (len f) + 1 and
A12: (Rev f) /. (n + 1) = f /. l9 by A4, Th4;
n + (1 + l9) = n + l by A6, A11;
hence |.(m - i).| + |.(k - j).| = 1 by A1, A8, A5, A7, A10, A12, A9, GOBOARD1:def 9; :: thesis: verum

end;

for n being Nat st n in dom (Rev f) holds
ex i, j being Nat st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) )

proof

let n be Nat; :: thesis: ( n in dom (Rev f) implies ex i, j being Nat st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) ) )
assume n in dom (Rev f) ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) )
then consider k being Nat such that
A13: k in dom f and
n + k = (len f) + 1 and
A14: (Rev f) /. n = f /. k by Th4;
consider i, j being Nat such that
A15: ( [i,j] in Indices G & f /. k = G * (i,j) ) by A1, A13, GOBOARD1:def 9;
take i ; :: thesis: ex j being Nat st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) )
take j ; :: thesis: ( [i,j] in Indices G & (Rev f) /. n = G * (i,j) )
thus ( [i,j] in Indices G & (Rev f) /. n = G * (i,j) ) by A14, A15; :: thesis: verum

end;

hence Rev f is_sequence_on G by A2, GOBOARD1:def 9; :: thesis: verum

end;

assume A16: Rev f is_sequence_on G ; :: thesis: f is_sequence_on G
A17: 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

proof

let n be Nat; :: thesis: ( n in dom f & n + 1 in dom f implies 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 )
assume that
A18: n in dom f and
A19: n + 1 in dom f ; :: thesis: 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
consider l being Nat such that
A20: l in dom (Rev f) and
A21: n + l = (len f) + 1 and
A22: f /. n = (Rev f) /. l by A18, Th3;
let m, k, i, j be Nat; :: thesis: ( [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) implies |.(m - i).| + |.(k - j).| = 1 )
assume A23: ( [m,k] in Indices G & [i,j] in Indices G & f /. n = G * (m,k) & f /. (n + 1) = G * (i,j) ) ; :: thesis: |.(m - i).| + |.(k - j).| = 1
A24: ( |.(i - m).| = |.(m - i).| & |.(j - k).| = |.(k - j).| ) by UNIFORM1:11;
consider l9 being Nat such that
A25: l9 in dom (Rev f) and
A26: (n + 1) + l9 = (len f) + 1 and
A27: f /. (n + 1) = (Rev f) /. l9 by A19, Th3;
n + (1 + l9) = n + l by A21, A26;
hence |.(m - i).| + |.(k - j).| = 1 by A16, A23, A20, A22, A25, A27, A24, GOBOARD1:def 9; :: thesis: verum

end;

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) )

proof

let n be Nat; :: thesis: ( n in dom f implies ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) ) )
assume n in dom f ; :: thesis: ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) )
then consider k being Nat such that
A28: k in dom (Rev f) and
n + k = (len f) + 1 and
A29: f /. n = (Rev f) /. k by Th3;
consider i, j being Nat such that
A30: ( [i,j] in Indices G & (Rev f) /. k = G * (i,j) ) by A16, A28, GOBOARD1:def 9;
take i ; :: thesis: ex j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) )
take j ; :: thesis: ( [i,j] in Indices G & f /. n = G * (i,j) )
thus ( [i,j] in Indices G & f /. n = G * (i,j) ) by A29, A30; :: thesis: verum

end;

hence f is_sequence_on G by A17, GOBOARD1:def 9; :: thesis: verum