let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: for G being Go-board st f is_sequence_on G holds
for i, j, k being Element of 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; :: thesis: ( f is_sequence_on G implies for i, j, k being Element of 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 ; :: thesis: for i, j, k being Element of 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 Element of NAT ; :: thesis: ( 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 and
A5: f /. k = G * i,j and
A6: f /. (k + 1) = G * i,(j + 1) ; :: thesis: i < len G
A7: ( 1 <= i & i <= len G & 1 <= j & j <= width G ) by A3, MATRIX_1:39;
assume i >= len G ; :: thesis: contradiction
then A8: i = len G by A7, XXREAL_0:1;
A9: right_cell f,k,G = cell G,i,j by A1, A2, A3, A4, A5, A6, GOBRD13:23;
L~ f is Bounded by JORDAN2C:73;
then A10: not (right_cell f,k,G) \ (L~ f) is Bounded by A7, A8, A9, JORDAN1B:37, TOPREAL6:99;
(right_cell f,k,G) \ (L~ f) c= RightComp f by A1, A2, JORDAN9:29;
then not RightComp f is Bounded by A10, JORDAN2C:16;
then not BDD (L~ f) is Bounded by GOBRD14:47;
hence contradiction by JORDAN2C:73, JORDAN2C:114; :: thesis: verum