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₁ being set st b₁ = JumpPart I holds
( b₁ is Function-like & b₁ is Relation-like ) ; :: thesis: verum