let n be Nat; :: 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 12;
A2: dom (Del (f,n9)) c= dom f by WSIERP_1:39;
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:104;
assume f . n in rng (Del (f,n)) ; :: thesis: contradiction
then consider j being object such that
A6: j in dom (Del (f,n)) and
A7: f . n = (Del (f,n)) . j by FUNCT_1:def 3;
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:110;
hence contradiction by A1, A3, A6, A2, A9, FUNCT_1:def 4; :: thesis: verum

end;

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

A11: j + 1 >= 0 + 1 by XREAL_1:6;
A12: j <= m by A8, FINSEQ_1:1;
then j + 1 <= m + 1 by XREAL_1:6;
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:111;
hence contradiction by A1, A3, A13, A14, FUNCT_1:def 4; :: thesis: verum

end;

end;