let i be Element of NAT ; :: thesis: for f being non constant standard clockwise_oriented special_circular_sequence st i in dom (GoB f) & f /. 1 = (GoB f) * i,(width (GoB f)) & f /. 1 = N-min (L~ f) holds
( f /. 2 = (GoB f) * (i + 1),(width (GoB f)) & f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) )
let f be non constant standard clockwise_oriented special_circular_sequence; :: thesis: ( i in dom (GoB f) & f /. 1 = (GoB f) * i,(width (GoB f)) & f /. 1 = N-min (L~ f) implies ( f /. 2 = (GoB f) * (i + 1),(width (GoB f)) & f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) ) )
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: ( f /. 2 = (GoB f) * (i + 1),(width (GoB f)) & f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) )
A4: i <= len (GoB f) by A1, FINSEQ_3:27;
4 < len f by GOBOARD7:36;
then A5: ((len f) -' 1) + 1 = len f by XREAL_1:237, XXREAL_0:2;
A6: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
A7: 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A8: 1 in dom f by FINSEQ_3:27;
A9: 1 <= width (GoB f) by GOBRD11:34;
A10: f /. 2 in N-most (L~ f) by A3, SPRECT_2:34;
A11: 1 + 1 <= len f by GOBOARD7:36, XXREAL_0:2;
then A12: 1 + 1 in dom f by FINSEQ_3:27;
then consider i1, j1 being Element of NAT such that
A13: [i1,j1] in Indices (GoB f) and
A14: f /. 2 = (GoB f) * i1,j1 by GOBOARD2:25;
A15: 1 <= j1 by A13, MATRIX_1:39;
A16: j1 <= width (GoB f) by A13, MATRIX_1:39;
A17: 1 <= i1 by A13, MATRIX_1:39;
A18: i1 <= len (GoB f) by A13, MATRIX_1:39;

now

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

end;

then A21: j1 = width (GoB f) by A16, XXREAL_0:1;

A22: now

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

end;

A23: 1 <= i by A1, FINSEQ_3:27;
then A24: [i,(width (GoB f))] in Indices (GoB f) by A9, A4, MATRIX_1:37;
(abs (i - i1)) + 0 = (abs (i - i1)) + (abs ((width (GoB f)) - (width (GoB f)))) by ABSVALUE:7
.= 1 by A2, A12, A13, A14, A8, A24, A21, GOBOARD5:13 ;
hence A25: f /. 2 = (GoB f) * (i + 1),(width (GoB f)) by A14, A21, A22, SEQM_3:81; :: thesis: f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1)
A26: (len f) -' 1 <= len f by NAT_D:44;
1 <= (len f) -' 1 by A11, NAT_D:49;
then A27: (len f) -' 1 in dom f by A26, FINSEQ_3:27;
then consider i2, j2 being Element of NAT such that
A28: [i2,j2] in Indices (GoB f) and
A29: f /. ((len f) -' 1) = (GoB f) * i2,j2 by GOBOARD2:25;
A30: 1 <= i2 by A28, MATRIX_1:39;
A31: j2 <= width (GoB f) by A28, MATRIX_1:39;
A32: i2 <= len (GoB f) by A28, MATRIX_1:39;
len f in dom f by A7, FINSEQ_3:27;
then A33: (abs (i2 - i)) + (abs (j2 - (width (GoB f)))) = 1 by A2, A24, A6, A5, A27, A28, A29, GOBOARD5:13;

per cases ( ( abs (i2 - i) = 1 & j2 = width (GoB f) ) or ( abs (j2 - (width (GoB f))) = 1 & i2 = i ) ) by A33, SEQM_3:82;

suppose that A34: abs (i2 - i) = 1 and
A35: j2 = width (GoB f) ; :: thesis: f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1)

(f /. ((len f) -' 1)) `2 = ((GoB f) * 1,(width (GoB f))) `2 by A9, A29, A30, A32, A35, GOBOARD5:2
.= (N-min (L~ f)) `2 by A2, A3, A9, A23, A4, GOBOARD5:2
.= N-bound (L~ f) by EUCLID:56 ;
then A36: f /. ((len f) -' 1) in N-most (L~ f) by A11, A27, GOBOARD1:16, SPRECT_2:14;

now

per cases ( i > i2 or i + 1 = i2 ) by A34, SEQM_3:81;

suppose i > i2 ; :: thesis: contradiction

then (f /. ((len f) -' 1)) `1 < (N-min (L~ f)) `1 by A2, A3, A9, A4, A29, A30, A35, GOBOARD5:4;
hence contradiction by A36, PSCOMP_1:98; :: thesis: verum

end;

suppose i + 1 = i2 ; :: thesis: contradiction

then 2 >= (len f) -' 1 by A25, A26, A29, A35, GOBOARD7:39;
then 2 + 1 >= len f by NAT_D:52;
hence contradiction by GOBOARD7:36, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

end;

suppose that A37: abs (j2 - (width (GoB f))) = 1 and
A38: i2 = i ; :: thesis: f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1)

width (GoB f) in NAT ;
then width (GoB f) = j2 + 1 by A31, A37, SEQM_3:81;
hence f /. ((len f) -' 1) = (GoB f) * i,((width (GoB f)) -' 1) by A29, A38, NAT_D:34; :: thesis: verum

end;

end;