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

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