let k be Element of 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:27;
then consider i1, j1 being Element of NAT such that
A4: [i1,j1] in Indices (GoB f) and
A5: f /. k = (GoB f) * i1,j1 by Th12;
k + 1 >= 1 by NAT_1:11;
then A6: k + 1 in dom f by A2, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A7: [i2,j2] in Indices (GoB f) and
A8: f /. (k + 1) = (GoB f) * i2,j2 by Th12;
A9: (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A8, Th13;

A10: now

per cases ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( i1 = i2 & abs (j1 - j2) = 1 ) ) by A9, GOBOARD1:2;

case that A11: abs (i1 - i2) = 1 and
A12: j1 = j2 ; :: thesis: ( ( i1 = i2 + 1 or i1 + 1 = i2 ) & j1 = j2 )

( i1 - i2 = 1 or - (i1 - i2) = 1 ) by A11, ABSVALUE:def 1;
hence ( i1 = i2 + 1 or i1 + 1 = i2 ) ; :: thesis: j1 = j2
thus j1 = j2 by A12; :: thesis: verum

end;

case that A13: i1 = i2 and
A14: abs (j1 - j2) = 1 ; :: thesis: ( ( j1 = j2 + 1 or j1 + 1 = j2 ) & i1 = i2 )

( j1 - j2 = 1 or - (j1 - j2) = 1 ) by A14, ABSVALUE:def 1;
hence ( j1 = j2 + 1 or j1 + 1 = j2 ) ; :: thesis: i1 = i2
thus i1 = i2 by A13; :: thesis: verum

end;

end;

end;

A15: 0 + 1 <= j1 by A4, MATRIX_1:39;
A16: j1 <= width (GoB f) by A4, MATRIX_1:39;
A17: 1 <= j2 by A7, MATRIX_1:39;
A18: j2 <= width (GoB f) by A7, MATRIX_1:39;
A19: 0 + 1 <= i1 by A4, MATRIX_1:39;
A20: i1 <= len (GoB f) by A4, MATRIX_1:39;
A21: 1 <= i2 by A7, MATRIX_1:39;
A22: i2 <= len (GoB f) by A7, MATRIX_1:39;
i1 > 0 by A19, NAT_1:13;
then consider i being Nat such that
A23: i + 1 = i1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A24: i + 1 = i1 by A23;
A25: i < len (GoB f) by A20, A23, NAT_1:13;
j1 > 0 by A15, NAT_1:13;
then consider j being Nat such that
A26: j + 1 = j1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A27: j + 1 = j1 by A26;
A28: j < width (GoB f) by A16, A26, NAT_1:13;

per cases ( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) ) by A10;

suppose A29: ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: (left_cell f,k) /\ (right_cell f,k) = LSeg f,k

then A30: j1 < width (GoB f) by A18, NAT_1:13;
A31: left_cell f,k = cell (GoB f),i,j1 by A1, A2, A4, A5, A7, A8, A23, A29, Th28;
right_cell f,k = cell (GoB f),i1,j1 by A1, A2, A4, A5, A7, A8, A24, A29, Th28;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * i1,j1),((GoB f) * i1,(j1 + 1)) by A15, A23, A25, A30, A31, Th26
.= LSeg f,k by A1, A2, A5, A8, A29, TOPREAL1:def 5 ;
:: thesis: verum

end;

suppose A32: ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: (left_cell f,k) /\ (right_cell f,k) = LSeg f,k

then A33: i1 < len (GoB f) by A22, NAT_1:13;
A34: left_cell f,k = cell (GoB f),i1,j1 by A1, A2, A4, A5, A7, A8, A27, A32, Th29;
right_cell f,k = cell (GoB f),i1,j by A1, A2, A4, A5, A7, A8, A26, A32, Th29;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * i1,j1),((GoB f) * (i1 + 1),j1) by A19, A26, A28, A33, A34, Th27
.= LSeg f,k by A1, A2, A5, A8, A32, TOPREAL1:def 5 ;
:: thesis: verum

end;

suppose A35: ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: (left_cell f,k) /\ (right_cell f,k) = LSeg f,k

then A36: i2 < len (GoB f) by A20, NAT_1:13;
A37: left_cell f,k = cell (GoB f),i2,j by A1, A2, A4, A5, A7, A8, A26, A35, Th30;
right_cell f,k = cell (GoB f),i2,j1 by A1, A2, A4, A5, A7, A8, A27, A35, Th30;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * (i2 + 1),j1),((GoB f) * i2,j1) by A21, A26, A28, A36, A37, Th27
.= LSeg f,k by A1, A2, A5, A8, A35, TOPREAL1:def 5 ;
:: thesis: verum

end;

suppose A38: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: (left_cell f,k) /\ (right_cell f,k) = LSeg f,k

then A39: j2 < width (GoB f) by A16, NAT_1:13;
A40: left_cell f,k = cell (GoB f),i1,j2 by A1, A2, A4, A5, A7, A8, A24, A38, Th31;
right_cell f,k = cell (GoB f),i,j2 by A1, A2, A4, A5, A7, A8, A23, A38, Th31;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * i1,(j2 + 1)),((GoB f) * i1,j2) by A17, A23, A25, A39, A40, Th26
.= LSeg f,k by A1, A2, A5, A8, A38, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;