theorem Th31: :: GOBOARD7:31

for f being V8() standard special_circular_sequence ex i being Nat st
( i in dom f & (f /. i) `2 <> (f /. 1) `2 )