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
A3: f | n is one-to-one by A1;
A4: <*p*> is one-to-one by FINSEQ_3:102;

now

let x be set ; :: 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:55;
then A5: not x in rng f by A2, TARSKI:def 1;
rng (f | n) c= rng f by Th21;
hence not x in rng (f | n) by A5; :: thesis: verum

end;

then rng (f | n) misses rng <*p*> by XBOOLE_0:3;
then A6: (f | n) ^ <*p*> is one-to-one by A3, A4, FINSEQ_3:98;
A7: f /^ n is one-to-one by A1;

now

let x be set ; :: thesis: ( x in rng (f /^ n) implies not x in rng ((f | n) ^ <*p*>) )
assume A8: x in rng (f /^ n) ; :: thesis: not x in rng ((f | n) ^ <*p*>)
rng (f | n) misses rng (f /^ n) by A1, Th37;
then A9: not x in rng (f | n) by A8, XBOOLE_0:3;
rng (f /^ n) c= rng f by Th36;
then x in rng f by A8;
then not x in {p} by A2, TARSKI:def 1;
then not x in rng <*p*> by FINSEQ_1:55;
then not x in (rng (f | n)) \/ (rng <*p*>) by A9, XBOOLE_0:def 3;
hence not x in rng ((f | n) ^ <*p*>) by FINSEQ_1:44; :: thesis: verum

end;

then rng ((f | n) ^ <*p*>) misses rng (f /^ n) by XBOOLE_0:3;
hence Ins f,n,p is one-to-one by A6, A7, FINSEQ_3:98; :: thesis: verum