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

( 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