consider
X
being non
empty
set
such that
A2
:
S
c=
[:
NAT
,
(
NAT
*
)
,
(
X
*
)
:]
by
Def1
;
I
in
S
;
then
JumpPart
I
in
NAT
*
by
A2
,
RECDEF_2:2
;
hence
for
b
_{1}
being
Function
st
b
_{1}
=
JumpPart
I
holds
b
_{1}
is
FinSequence-like
;
:: thesis:
verum