reconsider g = Sequel f as Real_Sequence by RSC;
Shift ((g | (Segm (len f))),1) is FinSequence of REAL by DBLSEQ_2:46;
hence Shift (f,1) is FinSequence-like ; :: thesis: verum