:: deftheorem Def1 defines Del WSIERP_1:def 1 :
for a being Nat
for fs being FinSequence
for b₃ being set holds
( ( not a in dom fs implies ( b₃ = Del (fs,a) iff b₃ = fs ) ) & ( a in dom fs implies ( b₃ = Del (fs,a) iff ( (len b₃) + 1 = len fs & ( for b being Nat holds
( ( b < a implies b₃ . b = fs . b ) & ( b >= a implies b₃ . b = fs . (b + 1) ) ) ) ) ) ) );