theorem Th4: :: MATRLIN:4

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