theorem Th1: :: LAPLACE:1

for f being FinSequence
for i being Nat st i in dom f holds
len (Del (f,i)) = (len f) -' 1