let f be MultOps of X,F; :: thesis: f is FinSequence-like
( dom F = dom f & dom F = Seg (len F) ) by Def1, FINSEQ_1:def 3;
hence f is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum