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 `1 = ((GoB h) * i,j) `1 & 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 `1 = ((GoB h) * i,j) `1 & 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 `1 = ((GoB h) * i,j) `1 & 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) `1 = ((GoB h) * i,j) `1 ) by Th11;
take q = h /. k; :: thesis: ( q `1 = ((GoB h) * i,j) `1 & q in L~ h )
thus q `1 = ((GoB h) * i,j) `1 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