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