let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: for n being Element of NAT st n < len f & len f > 4 holds
f | n is one-to-one
let n be Element of NAT ; :: thesis: ( n < len f & len f > 4 implies f | n is one-to-one )
assume that
A1: n < len f 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: 1 <= c1 by A3, FINSEQ_3:27;
A7: 1 <= c2 by A4, FINSEQ_3:27;
A8: c2 <= len (f | n) by A4, FINSEQ_3:27;
len (f | n) <= n by FINSEQ_5:19;
then c2 <= n by A8, XXREAL_0:2;
then A9: c2 < len f by A1, XXREAL_0:2;
A10: c1 <= len (f | n) by A3, FINSEQ_3:27;
len (f | n) <= n by FINSEQ_5:19;
then c1 <= n by A10, XXREAL_0:2;
then A11: c1 < len f by A1, XXREAL_0:2;
A12: ( (f | n) /. c1 = f /. c1 & (f | n) /. c2 = f /. c2 ) by A3, A4, FINSEQ_4:85;
assume A13: c1 <> c2 ; :: thesis: contradiction

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

suppose c1 < c2 ; :: thesis: contradiction

hence contradiction by A2, A5, A6, A9, A12, GOBOARD7:37; :: thesis: verum

end;

suppose c2 < c1 ; :: thesis: contradiction

hence contradiction by A2, A5, A7, A11, A12, GOBOARD7:37; :: thesis: verum

end;

end;

end;

hence f | n is one-to-one by PARTFUN2:16; :: thesis: verum