theorem Th30: :: JORDAN1H:30

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
( [(len G),i] in Indices G & G * ((len G),i) in rng f ) holds
proj1 .: (rng f) = proj1 .: (Values G)