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