theorem Th23: :: JORDAN1A:23

for t being Nat
for G being Go-board
for f being non constant standard special_circular_sequence st f is_sequence_on G & 1 <= t & t <= width G holds
(G * ((len G),t)) `1 >= E-bound (L~ f)