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