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