theorem Th31: :: JORDAN1H:31

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
( [i,1] in Indices G & G * (i,1) in rng f ) & ex i being Nat st
( [i,(width G)] in Indices G & G * (i,(width G)) in rng f ) holds
proj2 .: (rng f) = proj2 .: (Values G)