theorem Th21: :: GOBOARD1:28

for m, i being Nat
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st 1 <= len f & f /. (len f) in rng (Line (G,(len G))) & f is_sequence_on G & i in dom G & i + 1 in dom G & m in dom f & f /. m in rng (Line (G,i)) & ( for k being Nat st k in dom f & f /. k in rng (Line (G,i)) holds
k <= m ) holds
( m + 1 in dom f & f /. (m + 1) in rng (Line (G,(i + 1))) )