let D be non trivial set ; :: thesis: for f being non constant circular FinSequence of D holds len f > 2
let f be non constant circular FinSequence of D; :: thesis: len f > 2
assume A1: len f <= 2 ; :: thesis: contradiction

per cases ( len f < 1 + 1 or len f = 2 ) by A1, XXREAL_0:1;

suppose len f < 1 + 1 ; :: thesis: contradiction

then len f <= 1 by NAT_1:13;
then reconsider f = f as trivial Function by Th2;
f is constant ;
hence contradiction ; :: thesis: verum

end;

suppose A2: len f = 2 ; :: thesis: contradiction

then A3: dom f = {1,2} by FINSEQ_1:4, FINSEQ_1:def 3;
for n, m being Element of NAT st n in dom f & m in dom f holds
f . n = f . m

proof

let n, m be Element of NAT ; :: thesis: ( n in dom f & m in dom f implies f . n = f . m )
assume A4: ( n in dom f & m in dom f ) ; :: thesis: f . n = f . m

per cases ( ( n = 1 & m = 1 ) or ( n = 2 & m = 2 ) or ( n = 1 & m = 2 ) or ( n = 2 & m = 1 ) ) by A3, A4, TARSKI:def 2;

suppose ( ( n = 1 & m = 1 ) or ( n = 2 & m = 2 ) ) ; :: thesis: f . n = f . m

hence f . n = f . m ; :: thesis: verum

end;

suppose that A5: n = 1 and
A6: m = 2 ; :: thesis: f . n = f . m

A7: m in dom f by A3, A6, TARSKI:def 2;
n in dom f by A3, A5, TARSKI:def 2;
hence f . n = f /. 1 by A5, PARTFUN1:def 8
.= f /. (len f) by FINSEQ_6:def 1
.= f . m by A2, A6, A7, PARTFUN1:def 8 ;
:: thesis: verum

end;

suppose that A8: n = 2 and
A9: m = 1 ; :: thesis: f . n = f . m

A10: n in dom f by A3, A8, TARSKI:def 2;
m in dom f by A3, A9, TARSKI:def 2;
hence f . m = f /. 1 by A9, PARTFUN1:def 8
.= f /. (len f) by FINSEQ_6:def 1
.= f . n by A2, A8, A10, PARTFUN1:def 8 ;
:: thesis: verum

end;

end;

end;

hence contradiction by GOBOARD1:def 2; :: thesis: verum

end;

end;