theorem Th24: :: GOBOARD1:31

for n, 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 & i + 1 in dom f & n in Seg (width G) & f /. i in rng (Col (G,n)) & not f /. (i + 1) in rng (Col (G,n)) holds
for k being Nat st f /. (i + 1) in rng (Col (G,k)) & k in Seg (width G) holds
|.(n - k).| = 1