let f be non constant standard special_circular_sequence; :: thesis: for k being Nat st 1 <= k & k + 1 <= len f holds

( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex )

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex ) )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: ( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex )

left_cell (f,k) = left_cell (f,k,(GoB f)) by A1, A2, JORDAN1H:21;

hence left_cell (f,k,(GoB f)) is convex by A1, A2, Th21; :: thesis: right_cell (f,k,(GoB f)) is convex

k <= len f by A2, NAT_1:13;

then A3: ((len f) -' k) + k = len f by XREAL_1:235;

then A4: (len f) -' k >= 1 by A2, XREAL_1:6;

then A5: right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A3, GOBOARD9:10;

( len f = len (Rev f) & ((len f) -' k) + 1 <= len f ) by A1, A3, FINSEQ_5:def 3, XREAL_1:6;

then left_cell ((Rev f),((len f) -' k)) is convex by A4, Th21;

hence right_cell (f,k,(GoB f)) is convex by A1, A2, A5, JORDAN1H:23; :: thesis: verum

( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex )

let k be Nat; :: thesis: ( 1 <= k & k + 1 <= len f implies ( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex ) )

assume that

A1: 1 <= k and

A2: k + 1 <= len f ; :: thesis: ( left_cell (f,k,(GoB f)) is convex & right_cell (f,k,(GoB f)) is convex )

left_cell (f,k) = left_cell (f,k,(GoB f)) by A1, A2, JORDAN1H:21;

hence left_cell (f,k,(GoB f)) is convex by A1, A2, Th21; :: thesis: right_cell (f,k,(GoB f)) is convex

k <= len f by A2, NAT_1:13;

then A3: ((len f) -' k) + k = len f by XREAL_1:235;

then A4: (len f) -' k >= 1 by A2, XREAL_1:6;

then A5: right_cell (f,k) = left_cell ((Rev f),((len f) -' k)) by A1, A3, GOBOARD9:10;

( len f = len (Rev f) & ((len f) -' k) + 1 <= len f ) by A1, A3, FINSEQ_5:def 3, XREAL_1:6;

then left_cell ((Rev f),((len f) -' k)) is convex by A4, Th21;

hence right_cell (f,k,(GoB f)) is convex by A1, A2, A5, JORDAN1H:23; :: thesis: verum