consider X being non empty set such that
A2: the Instructions of S c= [:NAT,(NAT *),(X *):] by Def17;
I in the Instructions of S ;
then JumpPart I in NAT * by A2, RECDEF_2:2;
hence JumpPart I is FinSequence-like ; :: thesis: verum