theorem Th34: :: JORDAN1H:34

for f being non empty FinSequence of (TOP-REAL 2)
for G being Go-board st f is_sequence_on G & ex i being Nat st
( [1,i] in Indices G & G * (1,i) in rng f ) & ex i being Nat st
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) & ex i being Nat st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
G = GoB f