let k be Element of NAT ; :: thesis: for f being standard special_circular_sequence st 1 <= k & k + 1 <= len f holds
right_cell f,k,(GoB f) = right_cell f,k
let f be standard special_circular_sequence; :: thesis: ( 1 <= k & k + 1 <= len f implies right_cell f,k,(GoB f) = right_cell f,k )
assume that
A1: 1 <= k and
A2: k + 1 <= len f ; :: thesis: right_cell f,k,(GoB f) = right_cell f,k
set G = GoB f;
A3: f is_sequence_on GoB f by GOBOARD5:def 5;
for i1, j1, i2, j2 being Element of NAT st [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & right_cell f,k = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell f,k = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell f,k = cell (GoB f),i2,j2 ) holds
( i1 = i2 & j1 = j2 + 1 & right_cell f,k = cell (GoB f),(i1 -' 1),j2 )

proof

let i1, j1, i2, j2 be Element of NAT ; :: thesis: ( [i1,j1] in Indices (GoB f) & [i2,j2] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 & f /. (k + 1) = (GoB f) * i2,j2 & not ( i1 = i2 & j1 + 1 = j2 & right_cell f,k = cell (GoB f),i1,j1 ) & not ( i1 + 1 = i2 & j1 = j2 & right_cell f,k = cell (GoB f),i1,(j1 -' 1) ) & not ( i1 = i2 + 1 & j1 = j2 & right_cell f,k = cell (GoB f),i2,j2 ) implies ( i1 = i2 & j1 = j2 + 1 & right_cell f,k = cell (GoB f),(i1 -' 1),j2 ) )
assume that
A4: [i1,j1] in Indices (GoB f) and
A5: [i2,j2] in Indices (GoB f) and
A6: f /. k = (GoB f) * i1,j1 and
A7: f /. (k + 1) = (GoB f) * i2,j2 ; :: thesis: ( ( i1 = i2 & j1 + 1 = j2 & right_cell f,k = cell (GoB f),i1,j1 ) or ( i1 + 1 = i2 & j1 = j2 & right_cell f,k = cell (GoB f),i1,(j1 -' 1) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell f,k = cell (GoB f),i2,j2 ) or ( i1 = i2 & j1 = j2 + 1 & right_cell f,k = cell (GoB f),(i1 -' 1),j2 ) )
set IT = right_cell f,k;
right_cell f,k = right_cell f,k ;
then A8: ( ( i1 = i2 & j1 + 1 = j2 & right_cell f,k = cell (GoB f),i1,j1 ) or ( i1 + 1 = i2 & j1 = j2 & right_cell f,k = cell (GoB f),i1,(j1 -' 1) ) or ( i1 = i2 + 1 & j1 = j2 & right_cell f,k = cell (GoB f),i2,j2 ) or ( i1 = i2 & j1 = j2 + 1 & right_cell f,k = cell (GoB f),(i1 -' 1),j2 ) ) by A1, A2, A4, A5, A6, A7, GOBOARD5:def 6;
k < len f by A2, NAT_1:13;
then A9: k in dom f by A1, FINSEQ_3:27;
1 <= k + 1 by NAT_1:11;
then k + 1 in dom f by A2, FINSEQ_3:27;
then (abs (i1 - i2)) + (abs (j1 - j2)) = 1 by A3, A4, A5, A6, A7, A9, GOBOARD1:def 11;
then A10: ( ( abs (i1 - i2) = 1 & j1 = j2 ) or ( abs (j1 - j2) = 1 & i1 = i2 ) ) by GOBOARD1:2;

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, GOBOARD1:1;

case ( i1 = i2 & j1 + 1 = j2 ) ; :: thesis: right_cell f,k = cell (GoB f),i1,j1

hence right_cell f,k = cell (GoB f),i1,j1 by A8; :: thesis: verum

end;

case ( i1 + 1 = i2 & j1 = j2 ) ; :: thesis: right_cell f,k = cell (GoB f),i1,(j1 -' 1)

hence right_cell f,k = cell (GoB f),i1,(j1 -' 1) by A8; :: thesis: verum

end;

case ( i1 = i2 + 1 & j1 = j2 ) ; :: thesis: right_cell f,k = cell (GoB f),i2,j2

hence right_cell f,k = cell (GoB f),i2,j2 by A8; :: thesis: verum

end;

case ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis: right_cell f,k = cell (GoB f),(i1 -' 1),j2

hence right_cell f,k = cell (GoB f),(i1 -' 1),j2 by A8; :: thesis: verum

end;

end;

end;

hence right_cell f,k,(GoB f) = right_cell f,k by A1, A2, A3, GOBRD13:def 2; :: thesis: verum