dom f = Seg (len f) by FINSEQ_1:def 3;
hence Sum f is FinSequence-like by Def8; :: thesis: verum