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

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