theorem Th40: :: JORDAN1J:40

for G being Go-board
for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G holds
for i, j being Nat st 1 <= i & i <= len G & 1 <= j & j <= width G & G * (i,j) in L~ f holds
G * (i,j) in rng f