let D be non empty set ; 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; 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; ( f is_sequence_on G iff Rev f is_sequence_on G )
hereby ( Rev f is_sequence_on G implies f is_sequence_on G )
assume A1:
f is_sequence_on G
;
Rev f is_sequence_on GA2:
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;
( 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)
;
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;
( [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) )
;
|.(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;
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;
( 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)
;
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
;
ex j being Nat st
( [i,j] in Indices G & (Rev f) /. n = G * (i,j) )
take
j
;
( [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;
verum
end; hence
Rev f is_sequence_on G
by A2, GOBOARD1:def 9;
verum
end;
assume A16:
Rev f is_sequence_on G
; 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;
( 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
;
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;
( [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) )
;
|.(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;
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;
( 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
;
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
;
ex j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) )
take
j
;
( [i,j] in Indices G & f /. n = G * (i,j) )
thus
(
[i,j] in Indices G &
f /. n = G * (
i,
j) )
by A29, A30;
verum
end;
hence
f is_sequence_on G
by A17, GOBOARD1:def 9; verum