theorem Th1: :: MATRLIN:1

for n being Nat
for M being FinSequence st len M = n + 1 holds
len (Del (M,(n + 1))) = n