dom (f * h) = dom f by DR
.= Seg (len f) by FINSEQ_1:def 3 ;
hence f * h is FinSequence-like ; :: thesis: verum