theorem
for
f being non
constant standard special_circular_sequence for
k being
Nat st 1
<= k &
k + 2
<= len f holds
for
i being
Nat st 1
<= i &
i + 2
<= len (GoB f) &
f /. (k + 1) = (GoB f) * (
(i + 1),
(width (GoB f))) & ( (
f /. k = (GoB f) * (
(i + 2),
(width (GoB f))) &
f /. (k + 2) = (GoB f) * (
(i + 1),
((width (GoB f)) -' 1)) ) or (
f /. (k + 2) = (GoB f) * (
(i + 2),
(width (GoB f))) &
f /. k = (GoB f) * (
(i + 1),
((width (GoB f)) -' 1)) ) ) holds
LSeg (
((1 / 2) * (((GoB f) * (i,((width (GoB f)) -' 1))) + ((GoB f) * ((i + 1),(width (GoB f)))))),
(((1 / 2) * (((GoB f) * (i,(width (GoB f)))) + ((GoB f) * ((i + 1),(width (GoB f)))))) + |[0,1]|))
misses L~ f