let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st 1 <= n & len f > 4 holds
f /^ n is one-to-one
let n be Nat; :: thesis: ( 1 <= n & len f > 4 implies f /^ n is one-to-one )
assume that
A1: 1 <= n and
A2: len f > 4 ; :: thesis: f /^ n is one-to-one
for c1, c2 being Element of NAT st c1 in dom (f /^ n) & c2 in dom (f /^ n) & (f /^ n) /. c1 = (f /^ n) /. c2 holds
c1 = c2

proof

let c1, c2 be Element of NAT ; :: thesis: ( c1 in dom (f /^ n) & c2 in dom (f /^ n) & (f /^ n) /. c1 = (f /^ n) /. c2 implies c1 = c2 )
assume that
A3: c1 in dom (f /^ n) and
A4: c2 in dom (f /^ n) and
A5: (f /^ n) /. c1 = (f /^ n) /. c2 ; :: thesis: c1 = c2
A6: (f /^ n) /. c1 = f /. (c1 + n) by A3, FINSEQ_5:27;
A7: n <= len f by A3, RELAT_1:38, RFINSEQ:def 1;
then len (f /^ n) = (len f) - n by RFINSEQ:def 1;
then A8: (len (f /^ n)) + n = len f ;
len (f /^ n) = (len f) - n by A7, RFINSEQ:def 1;
then A9: (len (f /^ n)) + n = len f ;
c1 <= len (f /^ n) by A3, FINSEQ_3:25;
then A10: c1 + n <= len f by A9, XREAL_1:6;
0 + 1 <= c1 by A3, FINSEQ_3:25;
then A11: 1 + 0 < c1 + n by A1, XREAL_1:8;
A12: (f /^ n) /. c2 = f /. (c2 + n) by A4, FINSEQ_5:27;
c2 <= len (f /^ n) by A4, FINSEQ_3:25;
then A13: c2 + n <= len f by A8, XREAL_1:6;
0 + 1 <= c2 by A4, FINSEQ_3:25;
then A14: 1 + 0 < c2 + n by A1, XREAL_1:8;
assume A15: c1 <> c2 ; :: thesis: contradiction

per cases ( c1 < c2 or c2 < c1 ) by A15, XXREAL_0:1;

suppose c1 < c2 ; :: thesis: contradiction

then c1 + n < c2 + n by XREAL_1:6;
hence contradiction by A2, A5, A11, A13, A6, A12, Th23; :: thesis: verum

end;

suppose c2 < c1 ; :: thesis: contradiction

then c2 + n < c1 + n by XREAL_1:6;
hence contradiction by A2, A5, A14, A10, A6, A12, Th23; :: thesis: verum

end;

end;

end;

hence f /^ n is one-to-one by PARTFUN2:9; :: thesis: verum