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