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