let f be V8() standard special_circular_sequence; :: thesis: len (GoB f) > 1

A1: len (GoB f) <> 0 by MATRIX_0:def 10;

1 in dom f by FINSEQ_5:6;

then consider i2, j2 being Nat such that

A2: [i2,j2] in Indices (GoB f) and

A3: f /. 1 = (GoB f) * (i2,j2) by GOBOARD2:14;

A4: 1 <= i2 by A2, MATRIX_0:32;

assume len (GoB f) <= 1 ; :: thesis: contradiction

then A5: len (GoB f) = 1 by A1, NAT_1:25;

then i2 <= 1 by A2, MATRIX_0:32;

then A6: i2 = 1 by A4, XXREAL_0:1;

consider i being Nat such that

A7: i in dom f and

A8: (f /. i) `1 <> (f /. 1) `1 by Th30;

consider i1, j1 being Nat such that

A9: [i1,j1] in Indices (GoB f) and

A10: f /. i = (GoB f) * (i1,j1) by A7, GOBOARD2:14;

A11: ( 1 <= j1 & j1 <= width (GoB f) ) by A9, MATRIX_0:32;

A12: 1 <= i1 by A9, MATRIX_0:32;

i1 <= 1 by A5, A9, MATRIX_0:32;

then i1 = 1 by A12, XXREAL_0:1;

then A13: ((GoB f) * (i1,j1)) `1 = ((GoB f) * (1,1)) `1 by A5, A11, GOBOARD5:2;

( 1 <= j2 & j2 <= width (GoB f) ) by A2, MATRIX_0:32;

hence contradiction by A5, A8, A10, A3, A13, A6, GOBOARD5:2; :: thesis: verum

A1: len (GoB f) <> 0 by MATRIX_0:def 10;

1 in dom f by FINSEQ_5:6;

then consider i2, j2 being Nat such that

A2: [i2,j2] in Indices (GoB f) and

A3: f /. 1 = (GoB f) * (i2,j2) by GOBOARD2:14;

A4: 1 <= i2 by A2, MATRIX_0:32;

assume len (GoB f) <= 1 ; :: thesis: contradiction

then A5: len (GoB f) = 1 by A1, NAT_1:25;

then i2 <= 1 by A2, MATRIX_0:32;

then A6: i2 = 1 by A4, XXREAL_0:1;

consider i being Nat such that

A7: i in dom f and

A8: (f /. i) `1 <> (f /. 1) `1 by Th30;

consider i1, j1 being Nat such that

A9: [i1,j1] in Indices (GoB f) and

A10: f /. i = (GoB f) * (i1,j1) by A7, GOBOARD2:14;

A11: ( 1 <= j1 & j1 <= width (GoB f) ) by A9, MATRIX_0:32;

A12: 1 <= i1 by A9, MATRIX_0:32;

i1 <= 1 by A5, A9, MATRIX_0:32;

then i1 = 1 by A12, XXREAL_0:1;

then A13: ((GoB f) * (i1,j1)) `1 = ((GoB f) * (1,1)) `1 by A5, A11, GOBOARD5:2;

( 1 <= j2 & j2 <= width (GoB f) ) by A2, MATRIX_0:32;

hence contradiction by A5, A8, A10, A3, A13, A6, GOBOARD5:2; :: thesis: verum