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

A7: now

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

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

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

end;

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

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

end;

end;

end;

A12: ( 0 + 1 <= j1 & j1 <= width (GoB f) ) by A3, MATRIX_1:39;
A13: ( 1 <= j2 & j2 <= width (GoB f) ) by A5, MATRIX_1:39;
A14: ( 0 + 1 <= i1 & i1 <= len (GoB f) ) by A3, MATRIX_1:39;
A15: ( 1 <= i2 & i2 <= len (GoB f) ) by A5, MATRIX_1:39;
i1 > 0 by A14, NAT_1:13;
then consider i being Nat such that
A16: i + 1 = i1 by NAT_1:6;
reconsider i = i as Element of NAT by ORDINAL1:def 13;
A17: i + 1 = i1 by A16;
A18: i < len (GoB f) by A14, A16, NAT_1:13;
j1 > 0 by A12, NAT_1:13;
then consider j being Nat such that
A19: j + 1 = j1 by NAT_1:6;
reconsider j = j as Element of NAT by ORDINAL1:def 13;
A20: j + 1 = j1 by A19;
A21: j < width (GoB f) by A12, A19, 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 A7;

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

then A23: j1 < width (GoB f) by A13, NAT_1:13;
( left_cell f,k = cell (GoB f),i,j1 & right_cell f,k = cell (GoB f),i1,j1 ) by A1, A3, A5, A17, A22, Th28;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * i1,j1),((GoB f) * i1,(j1 + 1)) by A12, A16, A18, A23, Th26
.= LSeg f,k by A1, A3, A5, A22, TOPREAL1:def 5 ;
:: thesis: verum

end;

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

then A25: i1 < len (GoB f) by A15, NAT_1:13;
( left_cell f,k = cell (GoB f),i1,j1 & right_cell f,k = cell (GoB f),i1,j ) by A1, A3, A5, A20, A24, Th29;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * i1,j1),((GoB f) * (i1 + 1),j1) by A14, A19, A21, A25, Th27
.= LSeg f,k by A1, A3, A5, A24, TOPREAL1:def 5 ;
:: thesis: verum

end;

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

then A27: i2 < len (GoB f) by A14, NAT_1:13;
( left_cell f,k = cell (GoB f),i2,j & right_cell f,k = cell (GoB f),i2,j1 ) by A1, A3, A5, A20, A26, Th30;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * (i2 + 1),j1),((GoB f) * i2,j1) by A15, A19, A21, A27, Th27
.= LSeg f,k by A1, A3, A5, A26, TOPREAL1:def 5 ;
:: thesis: verum

end;

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

then A29: j2 < width (GoB f) by A12, NAT_1:13;
( left_cell f,k = cell (GoB f),i1,j2 & right_cell f,k = cell (GoB f),i,j2 ) by A1, A3, A5, A17, A28, Th31;
hence (left_cell f,k) /\ (right_cell f,k) = LSeg ((GoB f) * i1,(j2 + 1)),((GoB f) * i1,j2) by A13, A16, A18, A29, Th26
.= LSeg f,k by A1, A3, A5, A28, TOPREAL1:def 5 ;
:: thesis: verum

end;

end;