let h be non constant standard special_circular_sequence; :: thesis: for i, j being Element of 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 Element of 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 ( 1 <= i & i <= len (GoB h) & 1 <= j & 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 )
then consider k being Element of NAT such that
A1: ( k in dom h & [i,j] in Indices (GoB h) & (h /. k) `2 = ((GoB h) * i,j) `2 ) by Th12;
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 A1; :: thesis: q in L~ h
4 < len h by GOBOARD7:36;
hence q in L~ h by A1, GOBOARD1:16, XXREAL_0:2; :: thesis: verum