theorem Th23: :: GOBOARD1:30

for i being Nat
for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & i in dom f holds
ex n being Nat st
( n in Seg (width G) & f /. i in rng (Col (G,n)) )