let D be non trivial set ; :: thesis: for f being V25() circular FinSequence of D holds len f > 2
let f be V25() 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:2, FINSEQ_1:def 3;
for n, m being Nat st n in dom f & m in dom f holds
f . n = f . m
proof
let n, m be Nat; :: thesis: ( n in dom f & m in dom f implies f . n = f . m )
assume that
A4: n in dom f and
A5: 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, A5, 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 A6: n = 1 and
A7: m = 2 ; :: thesis: f . n = f . m
A8: m in dom f by A3, A7, TARSKI:def 2;
n in dom f by A3, A6, TARSKI:def 2;
hence f . n = f /. 1 by A6, PARTFUN1:def 6
.= f /. (len f) by FINSEQ_6:def 1
.= f . m by A2, A7, A8, PARTFUN1:def 6 ;
:: thesis: verum
end;
suppose that A9: n = 2 and
A10: m = 1 ; :: thesis: f . n = f . m
A11: n in dom f by A3, A9, TARSKI:def 2;
m in dom f by A3, A10, TARSKI:def 2;
hence f . m = f /. 1 by A10, PARTFUN1:def 6
.= f /. (len f) by FINSEQ_6:def 1
.= f . n by A2, A9, A11, PARTFUN1:def 6 ;
:: thesis: verum
end;
end;
end;
hence contradiction by SEQM_3:def 10; :: thesis: verum
end;
end;