let f be constant 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 ;

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

assume A4: card df <= 1 ; :: thesis: contradiction

per cases ( card df = 0 or card df = 1 ) by A4, NAT_1:25;

suppose card df = 0 ; :: thesis: contradiction

hence contradiction by A1; :: thesis: verum

end;

suppose card df = 1 ; :: thesis: contradiction

then consider x being object such that
A5: dom f = {x} by CARD_2:42;
n1 = x by A1, A5, TARSKI:def 1;
hence contradiction by A2, A5, TARSKI:def 1; :: thesis: verum

end;

end;

end;

dom f = Seg (len f) by FINSEQ_1:def 3;
hence len f > 1 by A3, FINSEQ_1:57; :: thesis: verum