theorem :: FINSEQ_5:87

for f being non empty FinSequence holds f = <*(f . 1)*> ^ (f /^ 1) by Th29a;