let f be Function; :: thesis: ( f = JumpPart I implies f is NAT -valued )
assume A1: f = JumpPart I ; :: thesis: f is NAT -valued
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 f is NAT -valued by A1, FINSEQ_1:def 11; :: thesis: verum