let D be non empty set ; for f being FinSequence of D
for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1))
let f be FinSequence of D; for p being Element of D
for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1))
let p be Element of D; for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1))
let n be Nat; ( n in dom f implies f = Del ((Ins (f,n,p)),(n + 1)) )
set fs1 = (f | n) ^ <*p*>;
set fs2 = f /^ n;
assume
n in dom f
; f = Del ((Ins (f,n,p)),(n + 1))
then
n in Seg (len f)
by FINSEQ_1:def 3;
then
n <= len f
by FINSEQ_1:1;
then A1:
len (f | n) = n
by FINSEQ_1:59;
len ((f | n) ^ <*p*>) =
(len (f | n)) + (len <*p*>)
by FINSEQ_1:22
.=
n + 1
by A1, FINSEQ_1:39
;
then Del ((Ins (f,n,p)),(n + 1)) =
(Del (((f | n) ^ <*p*>),(n + 1))) ^ (f /^ n)
by Lm42
.=
(f | n) ^ (f /^ n)
by A1, WSIERP_1:40
;
hence
f = Del ((Ins (f,n,p)),(n + 1))
by RFINSEQ:8; verum