theorem Th8: :: JORDAN5D:8

for f being non empty FinSequence of (TOP-REAL 2)
for j being Nat st 1 <= j & j <= width (GoB f) holds
ex k, i being Nat st
( k in dom f & [i,j] in Indices (GoB f) & f /. k = (GoB f) * (i,j) )