let n be Nat; :: thesis: for f being FinSequence st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
let f be FinSequence; :: thesis: ( f is one-to-one implies rng (f | n) misses rng (f /^ n) )
assume A1: f is one-to-one ; :: thesis: rng (f | n) misses rng (f /^ n)
A2: dom (f | n) c= dom f by Th18;
assume rng (f | n) meets rng (f /^ n) ; :: thesis: contradiction
then consider x being object such that
A3: x in rng (f | n) and
A4: x in rng (f /^ n) by XBOOLE_0:3;
consider i being object such that
A5: i in dom (f | n) and
A6: (f | n) . i = x by A3, FUNCT_1:def 3;
consider j being object such that
A7: j in dom (f /^ n) and
A8: (f /^ n) . j = x by A4, FUNCT_1:def 3;
reconsider ii = i, jj = j as Nat by A7, A5;
A9: jj + n in dom f by A7, Th26;

A10: now :: thesis: not ii = jj + n

( ii <= len (f | n) & len (f | n) <= n ) by A5, Th17, FINSEQ_3:25;
then A11: ii <= n by XXREAL_0:2;
assume A12: ii = jj + n ; :: thesis: contradiction
then n <= ii by NAT_1:11;
then i = n by A11, XXREAL_0:1;
then j = 0 by A12;
hence contradiction by A7, FINSEQ_3:25; :: thesis: verum

end;

f . (jj + n) = (f /^ n) . j by A7, Th27
.= f . i by A5, FUNCT_1:47, A6, A8 ;
hence contradiction by A1, A5, A2, A9, A10; :: thesis: verum