theorem Th28: :: SPRECT_3:28

for f being constant standard special_circular_sequence ex i being Nat st
( 1 <= i & i < len (GoB f) & N-min (L~ f) = (GoB f) * (i,(width (GoB f))) )