theorem Th27: :: GOBOARD1:34

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