dom (f +* (i,x)) = dom f by Th29
.= Seg (len f) by FINSEQ_1:def 3 ;
hence f +* (i,x) is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum