theorem Th7: :: JORDAN5D:7

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