dom f = Seg (len f) by FINSEQ_1:def 3;
hence r |^ f is FinSequence-like by Def4; :: thesis: verum