theorem :: TOPREAL8:36

for G being Go-board
for f being FinSequence of (TOP-REAL 2) st ( for n being Nat st n in dom f holds
ex i, j being Nat st
( [i,j] in Indices G & f /. n = G * (i,j) ) ) & f is constant & f is circular & f is unfolded & f is s.c.c. & f is special & len f > 4 holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is unfolded & g is s.c.c. & g is special & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )