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

consider n1, n2 being object such that

A1: n1 in dom f and

A2: ( n2 in dom f & f . n1 <> f . n2 ) by FUNCT_1:def 10;

reconsider df = dom f as finite set ;

hence len f > 1 by A3, FINSEQ_1:57; :: thesis: verum

consider n1, n2 being object such that

A1: n1 in dom f and

A2: ( n2 in dom f & f . n1 <> f . n2 ) by FUNCT_1:def 10;

reconsider df = dom f as finite set ;

A3: now :: thesis: not card df <= 1

dom f = Seg (len f)
by FINSEQ_1:def 3;assume A4:
card df <= 1
; :: thesis: contradiction

end;hence len f > 1 by A3, FINSEQ_1:57; :: thesis: verum