for D being set
for p being FinSequence of D
for i, j being Element of NAT st i in dom p & j in dom p & len (Del (p,i,j)) = 0 holds
( i = 1 & j = len p )