let f be V22() standard clockwise_oriented special_circular_sequence; for G being Go-board st f is_sequence_on G holds
for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G
let G be Go-board; ( f is_sequence_on G implies for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G )
assume A1:
f is_sequence_on G
; for i, j, k being Nat st 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) holds
i < len G
let i, j, k be Nat; ( 1 <= k & k + 1 <= len f & [i,j] in Indices G & [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) implies i < len G )
assume that
A2:
( 1 <= k & k + 1 <= len f )
and
A3:
[i,j] in Indices G
and
A4:
( [i,(j + 1)] in Indices G & f /. k = G * (i,j) & f /. (k + 1) = G * (i,(j + 1)) )
; i < len G
assume A5:
i >= len G
; contradiction
i <= len G
by A3, MATRIX_0:32;
then A6:
i = len G
by A5, XXREAL_0:1;
A7:
j <= width G
by A3, MATRIX_0:32;
right_cell (f,k,G) = cell (G,i,j)
by A1, A2, A3, A4, GOBRD13:22;
then
not (right_cell (f,k,G)) \ (L~ f) is bounded
by A7, A6, JORDAN1B:34, TOPREAL6:90;
then
not RightComp f is bounded
by A1, A2, JORDAN9:27, RLTOPSP1:42;
then
not BDD (L~ f) is bounded
by GOBRD14:37;
hence
contradiction
by JORDAN2C:106; verum