theorem :: PRE_POLY:13

for n being Nat
for M being FinSequence st len M = n + 1 holds
M = (Del (M,(len M))) ^ <*(M . (len M))*>