let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: for n being Nat st n in dom f holds
f = Del ((Ins (f,n,p)),(n + 1))
let n be Nat; :: thesis: ( 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 ; :: thesis: 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; :: thesis: verum