theorem Th10: :: JORDAN5D:10

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