theorem :: PRE_POLY:13

for M being FinSequence st M <> {} holds
M = (Del (M,(len M))) ^ <*(M . (len M))*>