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