theorem Th30: :: GOBOARD7:30

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