let f be circular s.c.c. FinSequence of (TOP-REAL 2); :: thesis: for n being Nat st n < len f & len f > 4 holds
f | n is one-to-one
let n be 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

A3: len (f | n) <= n by FINSEQ_5:17;
A4: len (f | n) <= n by FINSEQ_5:17;
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
A5: c1 in dom (f | n) and
A6: c2 in dom (f | n) and
A7: (f | n) /. c1 = (f | n) /. c2 ; :: thesis: c1 = c2
A8: 1 <= c1 by A5, FINSEQ_3:25;
c1 <= len (f | n) by A5, FINSEQ_3:25;
then c1 <= n by A3, XXREAL_0:2;
then A9: c1 < len f by A1, XXREAL_0:2;
A10: 1 <= c2 by A6, FINSEQ_3:25;
A11: (f | n) /. c1 = f /. c1 by A5, FINSEQ_4:70;
c2 <= len (f | n) by A6, FINSEQ_3:25;
then c2 <= n by A4, XXREAL_0:2;
then A12: c2 < len f by A1, XXREAL_0:2;
A13: (f | n) /. c2 = f /. c2 by A6, FINSEQ_4:70;
assume A14: c1 <> c2 ; :: thesis: contradiction

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

suppose c1 < c2 ; :: thesis: contradiction

hence contradiction by A2, A7, A8, A12, A11, A13, GOBOARD7:35; :: thesis: verum

end;

suppose c2 < c1 ; :: thesis: contradiction

hence contradiction by A2, A7, A10, A9, A11, A13, GOBOARD7:35; :: thesis: verum

end;

end;

end;

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