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) )
assume A2: n in dom f ; :: thesis: not f . n in rng (Del f,n)
then consider m being Nat such that
A3: ( len f = m + 1 & 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
A4: ( j in dom (Del f,n) & f . n = (Del f,n) . j ) by FUNCT_1:def 5;
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
A5: j in Seg m by A4, A3, FINSEQ_1:def 3;
reconsider j = j as Element of NAT by A4;
A6: dom (Del f,n') c= dom f by WSIERP_1:47;

per cases ( j < n' or j >= n' ) ;

suppose A7: j < n' ; :: thesis: contradiction

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

end;

suppose A8: j >= n' ; :: thesis: contradiction

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

end;

end;