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