let n be Nat; :: thesis: for D being non empty set
for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
let D be non empty set ; :: thesis: for p being Element of D
for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
let p be Element of D; :: thesis: for f being FinSequence of D st f is one-to-one & not p in rng f holds
Ins (f,n,p) is one-to-one
let f be FinSequence of D; :: thesis: ( f is one-to-one & not p in rng f implies Ins (f,n,p) is one-to-one )
assume that
A1: f is one-to-one and
A2: not p in rng f ; :: thesis: Ins (f,n,p) is one-to-one

now :: thesis: for x being object st x in rng (f /^ n) holds
not x in rng ((f | n) ^ <*p*>)

let x be object ; :: thesis: ( x in rng (f /^ n) implies not x in rng ((f | n) ^ <*p*>) )
assume A3: x in rng (f /^ n) ; :: thesis: not x in rng ((f | n) ^ <*p*>)
rng (f /^ n) c= rng f by Th33;
then x in rng f by A3;
then not x in {p} by A2, TARSKI:def 1;
then A4: not x in rng <*p*> by FINSEQ_1:38;
rng (f | n) misses rng (f /^ n) by A1, Th34;
then not x in rng (f | n) by A3, XBOOLE_0:3;
then not x in (rng (f | n)) \/ (rng <*p*>) by A4, XBOOLE_0:def 3;
hence not x in rng ((f | n) ^ <*p*>) by FINSEQ_1:31; :: thesis: verum

end;

then A5: rng ((f | n) ^ <*p*>) misses rng (f /^ n) by XBOOLE_0:3;

now :: thesis: for x being object st x in rng <*p*> holds
not x in rng (f | n)

let x be object ; :: thesis: ( x in rng <*p*> implies not x in rng (f | n) )
assume x in rng <*p*> ; :: thesis: not x in rng (f | n)
then x in {p} by FINSEQ_1:38;
then A6: not x in rng f by A2, TARSKI:def 1;
rng (f | n) c= rng f by Th19;
hence not x in rng (f | n) by A6; :: thesis: verum

end;

then ( <*p*> is one-to-one & rng (f | n) misses rng <*p*> ) by FINSEQ_3:93, XBOOLE_0:3;
then (f | n) ^ <*p*> is one-to-one by A1, FINSEQ_3:91;
hence Ins (f,n,p) is one-to-one by A1, A5, FINSEQ_3:91; :: thesis: verum