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

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