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