let n be Nat; :: thesis: for D being non empty set
for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
let D be non empty set ; :: thesis: for f being FinSequence of D st f is one-to-one holds
rng (f | n) misses rng (f /^ n)
let f be FinSequence of D; :: 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 Th20;
assume rng (f | n) meets rng (f /^ n) ; :: thesis: contradiction
then consider x being set such that
A3: x in rng (f | n) and
A4: x in rng (f /^ n) by XBOOLE_0:3;
consider i being Element of NAT such that
A5: i in dom (f | n) and
A6: (f | n) /. i = x by A3, PARTFUN2:4;
consider j being Element of NAT such that
A7: j in dom (f /^ n) and
A8: (f /^ n) /. j = x by A4, PARTFUN2:4;
A9: j + n in dom f by A7, Th29;

A10: now

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

end;

f /. (j + n) = (f /^ n) /. j by A7, Th30
.= f /. i by A5, A6, A8, FINSEQ_4:85 ;
hence contradiction by A1, A5, A2, A9, A10, PARTFUN2:17; :: thesis: verum