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