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)
assume rng (f | n) meets rng (f /^ n) ; :: thesis: contradiction
then consider x being set such that
A2: x in rng (f | n) and
A3: x in rng (f /^ n) by XBOOLE_0:3;
consider i being Element of NAT such that
A4: i in dom (f | n) and
A5: (f | n) /. i = x by A2, PARTFUN2:4;
consider j being Element of NAT such that
A6: j in dom (f /^ n) and
A7: (f /^ n) /. j = x by A3, PARTFUN2:4;
A8: dom (f | n) c= dom f by Th20;
A9: j + n in dom f by A6, Th29;
A10: f /. (j + n) = (f /^ n) /. j by A6, Th30
.= f /. i by A4, A5, A7, FINSEQ_4:85 ;

now

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

end;

hence contradiction by A1, A4, A8, A9, A10, PARTFUN2:17; :: thesis: verum