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:3;
then A1: len (f | n) = n by FINSEQ_1:80;
len ((f | n) ^ <*p*>) = (len (f | n)) + (len <*p*>) by FINSEQ_1:35
.= n + 1 by A1, FINSEQ_1:56 ;
then Del (Ins f,n,p),(n + 1) = (Del ((f | n) ^ <*p*>),(n + 1)) ^ (f /^ n) by Lm43
.= (f | n) ^ (f /^ n) by A1, WSIERP_1:48 ;
hence f = Del (Ins f,n,p),(n + 1) by RFINSEQ:21; :: thesis: verum