theorem :: GOBOARD3:2

for f being FinSequence of (TOP-REAL 2)
for G being Go-board 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 being_S-Seq holds
ex g being FinSequence of (TOP-REAL 2) st
( g is_sequence_on G & g is being_S-Seq & L~ f = L~ g & f /. 1 = g /. 1 & f /. (len f) = g /. (len g) & len f <= len g )