let k be Nat; :: thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
(left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
let f be standard special_circular_sequence; :: thesis: ( 1 <= k & k + 1 <= len f implies (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k) )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; :: thesis: (left_cell (f,k)) /\ (right_cell (f,k)) = LSeg (f,k)
k <= k + 1 by NAT_1:11;
then k <= len f by A2, XXREAL_0:2;
then A3: k in dom f by A1, FINSEQ_3:25;
then consider i1, j1 being Nat such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * (i1,j1) by Th11;
A6: k + 1 in dom f by A2, FINSEQ_3:25, NAT_1:11;
then consider i2, j2 being Nat such that
A7: [i2,j2] in Indices (GoB f) and
A8: f /. (k + 1) = (GoB f) * (i2,j2) by Th11;
A9: |.(i1 - i2).| + |.(j1 - j2).| = 1 by A3, A4, A5, A6, A7, A8, Th12;
A15: 0 + 1 <= j1 by A4, MATRIX_0:32;
A16: j1 <= width (GoB f) by A4, MATRIX_0:32;
A17: 1 <= j2 by A7, MATRIX_0:32;
A18: j2 <= width (GoB f) by A7, MATRIX_0:32;
A19: 0 + 1 <= i1 by A4, MATRIX_0:32;
A20: i1 <= len (GoB f) by A4, MATRIX_0:32;
A21: 1 <= i2 by A7, MATRIX_0:32;
A22: i2 <= len (GoB f) by A7, MATRIX_0:32;
i1 > 0 by A19;
then consider i being Nat such that
A23: i + 1 = i1 by NAT_1:6;
reconsider i = i as Nat ;
A24: i + 1 = i1 by A23;
A25: i < len (GoB f) by A20, A23, NAT_1:13;
j1 > 0 by A15;
then consider j being Nat such that
A26: j + 1 = j1 by NAT_1:6;
reconsider j = j as Nat ;
A27: j + 1 = j1 by A26;
A28: j < width (GoB f) by A16, A26, NAT_1:13;