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 `1 = ((GoB h) * (i,j)) `1 & 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 `1 = ((GoB h) * (i,j)) `1 & 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 `1 = ((GoB h) * (i,j)) `1 & 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) `1 = ((GoB h) * (i,j)) `1 by A1, A2, A3, A4, Th9;
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 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