consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
ex n being Nat st dom (Carrier f) = Seg n by A1, PRALG_1:def 14;
hence Carrier f is FinSequence-like by FINSEQ_1:def 2; :: thesis: verum