dom (r (#) f) = dom f by VFUNCT_1:def 4
.= Seg (len f) by FINSEQ_1:def 3 ;
hence r (#) f is FinSequence-like ; :: thesis: verum