theorem
for
i,
j,
k being
Nat for
f being
constant standard special_circular_sequence st 1
<= i &
i <= len (GoB f) & 1
<= j &
j + 1
< width (GoB f) & 1
<= k &
k + 1
< len f &
LSeg (
((GoB f) * (i,j)),
((GoB f) * (i,(j + 1))))
= LSeg (
f,
k) &
LSeg (
((GoB f) * (i,(j + 1))),
((GoB f) * (i,(j + 2))))
= LSeg (
f,
(k + 1)) holds
(
f /. k = (GoB f) * (
i,
j) &
f /. (k + 1) = (GoB f) * (
i,
(j + 1)) &
f /. (k + 2) = (GoB f) * (
i,
(j + 2)) )