let f be BinOps of a; :: thesis: f is FinSequence-like

( dom a = dom f & dom a = Seg (len a) ) by Def6, FINSEQ_1:def 3;

hence f is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum

( dom a = dom f & dom a = Seg (len a) ) by Def6, FINSEQ_1:def 3;

hence f is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum