let i be Nat; :: thesis: for f being 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 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:25;
4 < len f by GOBOARD7:34;
then A5: ((len f) -' 1) + 1 = len f by XREAL_1:235, XXREAL_0:2;
A6: f /. (len f) = f /. 1 by FINSEQ_6:def 1;
A7: 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A8: 1 in dom f by FINSEQ_3:25;
A9: 1 <= width (GoB f) by GOBRD11:34;
A10: f /. 2 in N-most (L~ f) by A3, SPRECT_2:30;
A11: 1 + 1 <= len f by GOBOARD7:34, XXREAL_0:2;
then A12: 1 + 1 in dom f by FINSEQ_3:25;
then consider i1, j1 being Nat such that
A13: [i1,j1] in Indices (GoB f) and
A14: f /. 2 = (GoB f) * (i1,j1) by GOBOARD2:14;
A15: 1 <= j1 by A13, MATRIX_0:32;
A16: j1 <= width (GoB f) by A13, MATRIX_0:32;
A17: 1 <= i1 by A13, MATRIX_0:32;
A18: i1 <= len (GoB f) by A13, MATRIX_0:32;

now :: thesis: not j1 < width (GoB f)

A19: (f /. 2) `2 = (N-min (L~ f)) `2 by A10, PSCOMP_1:39
.= N-bound (L~ f) by EUCLID:52 ;
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:1
.= N-bound (L~ f) by JORDAN5D:40 ;
hence contradiction by A14, A15, A17, A18, A20, A19, GOBOARD5:4; :: thesis: verum

end;

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

A22: now :: thesis: not i > i1

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

end;

A23: 1 <= i by A1, FINSEQ_3:25;
then A24: [i,(width (GoB f))] in Indices (GoB f) by A9, A4, MATRIX_0:30;
|.(i - i1).| + 0 = |.(i - i1).| + |.((width (GoB f)) - (width (GoB f))).| by ABSVALUE:2
.= 1 by A2, A12, A13, A14, A8, A24, A21, GOBOARD5:12 ;
hence A25: f /. 2 = (GoB f) * ((i + 1),(width (GoB f))) by A14, A21, A22, SEQM_3:41; :: 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:25;
then consider i2, j2 being Nat such that
A28: [i2,j2] in Indices (GoB f) and
A29: f /. ((len f) -' 1) = (GoB f) * (i2,j2) by GOBOARD2:14;
A30: 1 <= i2 by A28, MATRIX_0:32;
A31: j2 <= width (GoB f) by A28, MATRIX_0:32;
A32: i2 <= len (GoB f) by A28, MATRIX_0:32;
len f in dom f by A7, FINSEQ_3:25;
then A33: |.(i2 - i).| + |.(j2 - (width (GoB f))).| = 1 by A2, A24, A6, A5, A27, A28, A29, GOBOARD5:12;

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

suppose that A34: |.(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:1
.= (N-min (L~ f)) `2 by A2, A3, A9, A23, A4, GOBOARD5:1
.= N-bound (L~ f) by EUCLID:52 ;
then A36: f /. ((len f) -' 1) in N-most (L~ f) by A11, A27, GOBOARD1:1, SPRECT_2:10;

now :: thesis: contradiction

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

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:3;
hence contradiction by A36, PSCOMP_1:39; :: thesis: verum

end;

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

then 2 >= (len f) -' 1 by A25, A26, A29, A35, GOBOARD7:37;
then 2 + 1 >= len f by NAT_D:52;
hence contradiction by GOBOARD7:34, 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: |.(j2 - (width (GoB f))).| = 1 and
A38: i2 = i ; :: thesis: f /. ((len f) -' 1) = (GoB f) * (i,((width (GoB f)) -' 1))

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

end;

end;