let f be non constant standard special_circular_sequence; :: thesis: width (GoB f) > 1
A1: width (GoB f) <> 0 by GOBOARD1:def 5;
1 in dom f by FINSEQ_5:6;
then consider i2, j2 being Element of NAT such that
A2: [i2,j2] in Indices (GoB f) and
A3: f /. 1 = (GoB f) * i2,j2 by GOBOARD2:25;
A4: 1 <= j2 by A2, MATRIX_1:39;
assume width (GoB f) <= 1 ; :: thesis: contradiction
then A5: width (GoB f) = 1 by A1, NAT_1:26;
then j2 <= 1 by A2, MATRIX_1:39;
then A6: j2 = 1 by A4, XXREAL_0:1;
consider i being Element of NAT such that
A7: i in dom f and
A8: (f /. i) `2 <> (f /. 1) `2 by Th33;
consider i1, j1 being Element of NAT such that
A9: [i1,j1] in Indices (GoB f) and
A10: f /. i = (GoB f) * i1,j1 by A7, GOBOARD2:25;
A11: ( 1 <= i1 & i1 <= len (GoB f) ) by A9, MATRIX_1:39;
A12: 1 <= j1 by A9, MATRIX_1:39;
j1 <= 1 by A5, A9, MATRIX_1:39;
then j1 = 1 by A12, XXREAL_0:1;
then A13: ((GoB f) * i1,j1) `2 = ((GoB f) * 1,1) `2 by A5, A11, GOBOARD5:2;
( 1 <= i2 & i2 <= len (GoB f) ) by A2, MATRIX_1:39;
hence contradiction by A5, A8, A10, A3, A13, A6, GOBOARD5:2; :: thesis: verum