A1: dom (</> f) = dom f by Def34;
ex n being Nat st dom f = Seg n by FINSEQ_1:def 2;
hence </> f is FinSequence-like by A1, FINSEQ_1:def 2; :: thesis: verum