theorem :: GOBOARD1:25

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 Seg (width G) & rng f misses rng (Col (G,i)) & width G > 1 holds
f is_sequence_on DelCol (G,i)