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 Element of NAT st n in dom (Rev f) & n + 1 in dom (Rev f) holds
for m, k, i, j being Element of 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
(abs (m - i)) + (abs (k - j)) = 1

proof

let n be Element of NAT ; :: thesis: ( n in dom (Rev f) & n + 1 in dom (Rev f) implies for m, k, i, j being Element of 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
(abs (m - i)) + (abs (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 Element of 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
(abs (m - i)) + (abs (k - j)) = 1
consider l being Element of NAT such that
A5: l in dom f and
A6: n + l = (len f) + 1 and
A7: (Rev f) /. n = f /. l by A3, Th6;
let m, k, i, j be Element of 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 (abs (m - i)) + (abs (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: (abs (m - i)) + (abs (k - j)) = 1
A9: ( abs (i - m) = abs (m - i) & abs (j - k) = abs (k - j) ) by UNIFORM1:11;
consider l9 being Element of 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, Th6;
n + (1 + l9) = n + l by A6, A11;
hence (abs (m - i)) + (abs (k - j)) = 1 by A1, A8, A5, A7, A10, A12, A9, GOBOARD1:def 9; :: thesis: verum

end;

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

proof

let n be Element of NAT ; :: thesis: ( n in dom (Rev f) implies ex i, j being Element of NAT st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) ) )
assume n in dom (Rev f) ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) )
then consider k being Element of NAT such that
A13: k in dom f and
n + k = (len f) + 1 and
A14: (Rev f) /. n = f /. k by Th6;
consider i, j being Element of 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 Element of 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 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

proof

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

end;

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

proof

let n be Element of NAT ; :: thesis: ( n in dom f implies ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) ) )
assume n in dom f ; :: thesis: ex i, j being Element of NAT st
( [i,j] in Indices G & f /. n = G * (i,j) )
then consider k being Element of NAT such that
A28: k in dom (Rev f) and
n + k = (len f) + 1 and
A29: f /. n = (Rev f) /. k by Th5;
consider i, j being Element of 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 Element of 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