let f be V8() standard special_circular_sequence; 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
; 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; verum