consider n being Nat such that
A1: dom p = Seg n by FINSEQ_1:def 2;
dom (Carrier p) = dom p by Def13;
hence Carrier p is FinSequence-like by A1, FINSEQ_1:def 2; :: thesis: verum