let i be Element of NAT ; :: thesis:
let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis:
assume that
A1: i in dom (GoB f) and
A2: f /. 1 = (GoB f) * i,(width (GoB f)) and
A3: f /. 1 = N-min (L~ f) ; :: thesis:
A4: f /. 2 in N-most (L~ f) by A3, SPRECT_2:34;
A5: 1 <= width (GoB f) by GOBRD11:34;
A6: 4 < len f by GOBOARD7:36;
A7: 1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A8: 1 + 1 in dom f by FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A9: [i1,j1] in Indices (GoB f) and
A10: f /. 2 = (GoB f) * i1,j1 by GOBOARD2:25;
A11: 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A12: 1 in dom f by FINSEQ_3:27;
A13: ( 1 <= i & i <= len (GoB f) ) by A1, FINSEQ_3:27;
then A14: [i,(width (GoB f))] in Indices (GoB f) by A5, MATRIX_1:37;
A15: ( 1 <= j1 & j1 <= width (GoB f) ) by A9, MATRIX_1:39;
A16: ( 1 <= i1 & i1 <= len (GoB f) ) by A9, MATRIX_1:39;

now

assume A17: j1 < width (GoB f) ; :: thesis:
A18: ((GoB f) * i1,(width (GoB f))) `2 = ((GoB f) * 1,(width (GoB f))) `2 by A5, A16, GOBOARD5:2
.= N-bound (L~ f) by JORDAN5D:42 ;
(f /. 2) `2 = (N-min (L~ f)) `2 by A4, PSCOMP_1:98
.= N-bound (L~ f) by EUCLID:56 ;
hence contradiction by A10, A15, A16, A17, A18, GOBOARD5:5; :: thesis:

end;

then A19: j1 = width (GoB f) by A15, XXREAL_0:1;
A20: (abs (i - i1)) + 0 = (abs (i - i1)) + (abs ((width (GoB f)) - (width (GoB f)))) by ABSVALUE:7
.= 1 by A2, A8, A9, A10, A12, A14, A19, GOBOARD5:13 ;

now

assume i > i1 ; :: thesis:
then (f /. 2) `1 < (N-min (L~ f)) `1 by A2, A3, A10, A13, A15, A16, A19, GOBOARD5:4;
hence contradiction by A4, PSCOMP_1:98; :: thesis:

end;

hence A21: f /. 2 = (GoB f) * (i + 1),(width (GoB f)) by A10, A19, A20, GOBOARD1:1; :: thesis:
A22: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
A23: ((len f) -' 1) + 1 = len f by A6, XREAL_1:237, XXREAL_0:2;
A24: ( 1 <= (len f) -' 1 & (len f) -' 1 <= len f ) by A7, NAT_D:44, NAT_D:49;
then A25: (len f) -' 1 in dom f by FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A26: [i2,j2] in Indices (GoB f) and
A27: f /. ((len f) -' 1) = (GoB f) * i2,j2 by GOBOARD2:25;
A28: ( 1 <= i2 & i2 <= len (GoB f) ) by A26, MATRIX_1:39;
A29: ( 1 <= j2 & j2 <= width (GoB f) ) by A26, MATRIX_1:39;
len f in dom f by A11, FINSEQ_3:27;
then A30: (abs (i2 - i)) + (abs (j2 - (width (GoB f)))) = 1 by A2, A14, A22, A23, A25, A26, A27, GOBOARD5:13;

per cases by A30, GOBOARD1:2;

suppose that A31: abs (i2 - i) = 1 and
A32: j2 = width (GoB f) ; :: thesis:

(f /. ((len f) -' 1)) `2 = ((GoB f) * 1,(width (GoB f))) `2 by A5, A27, A28, A32, GOBOARD5:2
.= (N-min (L~ f)) `2 by A2, A3, A5, A13, GOBOARD5:2
.= N-bound (L~ f) by EUCLID:56 ;
then A33: f /. ((len f) -' 1) in N-most (L~ f) by A7, A25, GOBOARD1:16, SPRECT_2:14;

now

per cases by A31, GOBOARD1:1;

suppose i > i2 ; :: thesis:

then (f /. ((len f) -' 1)) `1 < (N-min (L~ f)) `1 by A2, A3, A5, A13, A27, A28, A32, GOBOARD5:4;
hence contradiction by A33, PSCOMP_1:98; :: thesis:

end;

suppose i + 1 = i2 ; :: thesis:

then 2 >= (len f) -' 1 by A21, A24, A27, A32, GOBOARD7:39;
then 2 + 1 >= len f by NAT_D:52;
hence contradiction by GOBOARD7:36, XXREAL_0:2; :: thesis:

end;

hence f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) ; :: thesis:

end;

suppose that A34: abs (j2 - (width (GoB f))) = 1 and
A35: i2 = i ; :: thesis:

width (GoB f) in NAT ;
then ( j2 < width (GoB f) & width (GoB f) = j2 + 1 ) by A29, A34, GOBOARD1:1;
hence f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) by A27, A35, NAT_D:34; :: thesis:

end;