theorem :: FINSEQ_5:86

for f being non empty FinSequence holds f = <*(f . 1)*> ^ (Del (f,1))