let h be non constant standard special_circular_sequence; :: thesis: for i, j being Nat st 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) holds

ex q being Point of (TOP-REAL 2) st

( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

let i, j be Nat; :: thesis: ( 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) implies ex q being Point of (TOP-REAL 2) st

( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) )

assume that

A1: 1 <= i and

A2: i <= len (GoB h) and

A3: 1 <= j and

A4: j <= width (GoB h) ; :: thesis: ex q being Point of (TOP-REAL 2) st

( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

consider k being Nat such that

A5: k in dom h and

[i,j] in Indices (GoB h) and

A6: (h /. k) `2 = ((GoB h) * (i,j)) `2 by A1, A2, A3, A4, Th10;

take q = h /. k; :: thesis: ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

thus q `2 = ((GoB h) * (i,j)) `2 by A6; :: thesis: q in L~ h

4 < len h by GOBOARD7:34;

hence q in L~ h by A5, GOBOARD1:1, XXREAL_0:2; :: thesis: verum

ex q being Point of (TOP-REAL 2) st

( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

let i, j be Nat; :: thesis: ( 1 <= i & i <= len (GoB h) & 1 <= j & j <= width (GoB h) implies ex q being Point of (TOP-REAL 2) st

( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h ) )

assume that

A1: 1 <= i and

A2: i <= len (GoB h) and

A3: 1 <= j and

A4: j <= width (GoB h) ; :: thesis: ex q being Point of (TOP-REAL 2) st

( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

consider k being Nat such that

A5: k in dom h and

[i,j] in Indices (GoB h) and

A6: (h /. k) `2 = ((GoB h) * (i,j)) `2 by A1, A2, A3, A4, Th10;

take q = h /. k; :: thesis: ( q `2 = ((GoB h) * (i,j)) `2 & q in L~ h )

thus q `2 = ((GoB h) * (i,j)) `2 by A6; :: thesis: q in L~ h

4 < len h by GOBOARD7:34;

hence q in L~ h by A5, GOBOARD1:1, XXREAL_0:2; :: thesis: verum