let n be natural number ; :: thesis: for f being FinSequence st f is one-to-one & n in dom f holds
not f . n in rng (Del f,n)
let f be FinSequence; :: thesis: ( f is one-to-one & n in dom f implies not f . n in rng (Del f,n) )
assume A1: f is one-to-one ; :: thesis: ( not n in dom f or not f . n in rng (Del f,n) )
reconsider n9 = n as Element of NAT by ORDINAL1:def 13;
A2: dom (Del f,n9) c= dom f by WSIERP_1:47;
assume A3: n in dom f ; :: thesis: not f . n in rng (Del f,n)
then consider m being Nat such that
A4: len f = m + 1 and
A5: len (Del f,n) = m by FINSEQ_3:113;
assume f . n in rng (Del f,n) ; :: thesis: contradiction
then consider j being set such that
A6: j in dom (Del f,n) and
A7: f . n = (Del f,n) . j by FUNCT_1:def 5;
A8: j in Seg m by A5, A6, FINSEQ_1:def 3;
reconsider j = j as Element of NAT by A6;

per cases ( j < n9 or j >= n9 ) ;

suppose A9: j < n9 ; :: thesis: contradiction

then f . n = f . j by A7, FINSEQ_3:119;
hence contradiction by A1, A3, A6, A2, A9, FUNCT_1:def 8; :: thesis: verum

end;

suppose A10: j >= n9 ; :: thesis: contradiction

A11: j + 1 >= 0 + 1 by XREAL_1:8;
A12: j <= m by A8, FINSEQ_1:3;
then j + 1 <= m + 1 by XREAL_1:8;
then j + 1 in Seg (m + 1) by A11;
then A13: j + 1 in dom f by A4, FINSEQ_1:def 3;
A14: j + 1 <> n by A10, NAT_1:13;
f . n = f . (j + 1) by A3, A4, A7, A10, A12, FINSEQ_3:120;
hence contradiction by A1, A3, A13, A14, FUNCT_1:def 8; :: thesis: verum

end;

end;